model_parser.ml 12.5 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

open Stdlib
13
open Format
14 15 16 17
open Term
open Ident
open Printer

18 19 20 21 22 23
(*
let debug = Debug.register_info_flag "model_parser"
  ~desc:"Print@ debugging@ messages@ about@ parsing@ \
         the@ counter-example@ model."
*)

24
(*
25
***************************************************************
26 27 28
**  Counter-example model values
****************************************************************
*)
29 30 31 32

type model_value =
 | Integer of string
 | Array of model_array
33
 | Unparsed of string
34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49
and  arr_index = {
  arr_index_key : int;
  arr_index_value : model_value;
}
and model_array = {
  arr_others  : model_value;
  arr_indices : arr_index list;
}

let array_create_constant ~value =
  {
    arr_others = value;
    arr_indices = [];
  }

let array_add_element ~array ~index ~value =
50 51
  (*
     Adds the element value to the array on specified index.
52 53 54 55 56 57 58 59 60 61 62 63 64
  *)
  let int_index = match index with
    | Integer s -> int_of_string s
    | _ -> raise Not_found in
  let arr_index = {
    arr_index_key = int_index;
    arr_index_value = value
  } in
  {
    arr_others = array.arr_others;
    arr_indices = arr_index::array.arr_indices;
  }

65
let rec print_indices sanit_print fmt indices =
66 67 68 69
  match indices with
  | [] -> ()
  | index::tail ->
    fprintf fmt "; %d -> " index.arr_index_key;
70 71
    print_model_value_sanit sanit_print fmt index.arr_index_value;
    print_indices sanit_print fmt tail
72
and
73
print_array sanit_print fmt arr =
74
  fprintf fmt "{others -> ";
75 76
  print_model_value_sanit sanit_print fmt arr.arr_others;
  print_indices sanit_print fmt arr.arr_indices;
77 78
  fprintf fmt "}"
and
79
print_model_value_sanit sanit_print fmt value =
80 81
  (* Prints model value. *)
  match value with
82
  | Integer s -> sanit_print fmt s
83
  | Unparsed s -> sanit_print fmt s
84 85 86 87
  | Array a -> print_array sanit_print fmt a

let print_model_value fmt value =
  print_model_value_sanit (fun fmt s -> fprintf fmt "%s" s) fmt value
88

89 90

(*
91
***************************************************************
92 93 94
**  Model elements
***************************************************************
*)
95 96 97 98 99
type model_element_type =
| Result
| Old
| Other

100
type model_element = {
101
  me_name     : string;
102
  me_type     : model_element_type;
103
  me_value    : model_value;
104 105
  me_location : Loc.position option;
  me_term     : Term.term option;
106
}
107

108 109 110 111 112 113 114 115 116
let split_me_name name =
  let splitted = Str.bounded_split (Str.regexp_string "@") name 2 in
  match splitted with
  | [first] -> (first, "")
  | first::[second] ->
    (first, second)
  | _ -> (* here, "_" can only stand for [] *)
    ("", "")

117
let create_model_element ~name ~value ?location ?term () =
118 119 120 121 122
  let (name, type_s) = split_me_name name in
  let t = match type_s with
    | "result" -> Result
    | "old" -> Old
    | _ -> Other in
123 124
  {
    me_name = name;
125
    me_type = t;
126 127
    me_value = value;
    me_location = location;
128
    me_term = term;
129 130
  }

131
(*
132 133 134 135
let print_location fmt m_element =
    match m_element.me_location with
    | None -> fprintf fmt "\"no location\""
    | Some loc -> Loc.report_position fmt loc
136
*)
137 138

(*
139
***************************************************************
140 141
**  Model definitions
***************************************************************
142
*)
143 144 145 146 147 148 149 150 151 152 153 154 155 156
module IntMap = Map.Make(struct type t  = int let compare = compare end)
module StringMap = Map.Make(String)

type model_file = model_element list IntMap.t
type model = model_file StringMap.t

let empty_model = StringMap.empty
let empty_model_file = IntMap.empty

type model_parser =  string -> Printer.printer_mapping -> model

type raw_model_parser =  string -> model_element list

(*
157
***************************************************************
158 159 160
**  Quering the model
***************************************************************
*)
161 162
let print_model_element me_name_trans fmt m_element =
  let me_name = me_name_trans (m_element.me_name, m_element.me_type) in
163
  fprintf fmt  "%s = %a"
164
      me_name print_model_value m_element.me_value
165

166 167
let print_model_elements ?(sep = "\n") me_name_trans fmt m_elements =
  Pp.print_list (fun fmt () -> Pp.string fmt sep) (print_model_element me_name_trans) fmt m_elements
168

169 170
let print_model_file fmt me_name_trans filename model_file =
  fprintf fmt "File %s:" filename;
171
  IntMap.iter
172
    (fun line m_elements ->
173 174
      fprintf fmt "\nLine %d:\n" line;
      print_model_elements me_name_trans fmt m_elements)
175
    model_file
176

177 178 179 180 181 182 183 184 185
let why_name_trans (me_name, me_type) =
  match me_type with
  | Result -> "result"
  | Old -> "old" ^ " " ^ me_name
  | Other -> me_name

let print_model
    ?(me_name_trans = why_name_trans)
    fmt
186
    model =
187
  StringMap.iter (print_model_file fmt me_name_trans) model
188

189 190 191
let model_to_string
    ?(me_name_trans = why_name_trans)
    model =
192
  print_model ~me_name_trans str_formatter model;
193 194
  flush_str_formatter ()

195 196 197 198 199
let get_model_file model filename =
  try
    StringMap.find filename model
  with Not_found ->
    empty_model_file
200

201 202 203 204 205
let get_elements model_file line_number =
  try
    IntMap.find line_number model_file
  with Not_found ->
    []
206

207
let get_padding line =
208
  try
209 210 211 212 213
    let r = Str.regexp " *" in
    ignore (Str.search_forward r line 0);
    Str.matched_string line
  with Not_found -> ""

214 215 216 217 218 219 220
let interleave_line
    start_comment
    end_comment
    me_name_trans
    model_file
    (source_code, line_number)
    line =
221 222
  try
    let model_elements = IntMap.find line_number model_file in
223
    print_model_elements me_name_trans str_formatter model_elements ~sep:"; ";
224
    let cntexmp_line =
225
      (get_padding line) ^
226 227
	start_comment ^
	(flush_str_formatter ()) ^
228
	end_comment in
229

230
    (source_code ^ line ^ cntexmp_line ^ "\n", line_number + 1)
231 232 233
  with Not_found ->
    (source_code ^ line, line_number + 1)

234 235 236 237

let interleave_with_source
    ?(start_comment="(* ")
    ?(end_comment=" *)")
238
    ?(me_name_trans = why_name_trans)
239
    model
240 241
    ~filename
    ~source_code =
242 243 244 245
  try
    let model_file = StringMap.find  filename model in
    let lines = Str.split (Str.regexp "^") source_code in
    let (source_code, _) = List.fold_left
246 247
      (interleave_line
	 start_comment end_comment me_name_trans model_file)
248 249
      ("", 1)
      lines in
250 251 252
    source_code
  with Not_found ->
    source_code
253 254 255 256 257


(*
**  Quering the model - json
*)
258
let print_model_value_json fmt me_value =
259 260
  fprintf fmt "%a" (print_model_value_sanit Json.string) me_value

261
let model_elements_to_map_bindings model_elements =
262
  List.fold_left
263
    (fun map_bindings me ->
264
      (me, me.me_value)::map_bindings
265
    )
266
    []
267 268
    model_elements

269
let print_model_elements_json me_name_to_str fmt model_elements =
270
  Json.map_bindings
271
    me_name_to_str
272 273 274
    print_model_value_json
    fmt
    (model_elements_to_map_bindings model_elements)
275

276
let print_model_elements_on_lines_json me_name_to_str fmt model_file =
277 278
  Json.map_bindings
    (fun i -> string_of_int i)
279
    (print_model_elements_json me_name_to_str)
280 281
    fmt
    (IntMap.bindings model_file)
282

283 284 285
let print_model_json
    ?(me_name_trans = why_name_trans)
    fmt
286
    model =
287 288
  let me_name_to_str = fun me ->
    me_name_trans (me.me_name, me.me_type) in
289 290
  Json.map_bindings
    (fun s -> s)
291
    (print_model_elements_on_lines_json me_name_to_str)
292
    fmt
293
    (StringMap.bindings model)
294

295 296 297
let model_to_string_json
    ?(me_name_trans = why_name_trans)
    model =
298
  print_model_json str_formatter ~me_name_trans model;
299
  flush_str_formatter ()
300

301

302
(*
303
***************************************************************
304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324
**  Building the model from raw model
***************************************************************
*)

let add_to_model model model_element =
  match model_element.me_location with
  | None -> model
  | Some pos ->
    let (filename, line_number, _, _) = Loc.get pos in
    let model_file = get_model_file model filename in
    let elements = get_elements model_file line_number in
    let elements = model_element::elements in
    let model_file = IntMap.add line_number elements model_file in
    StringMap.add filename model_file model

(* Estabilish mapping to why3 code *)
let rec extract_element_name labels raw_string regexp =
  match labels with
  | [] -> raw_string
  | label::labels_tail ->
    let l_string = label.lab_string in
325 326
    begin
      try
327 328 329 330 331
	ignore(Str.search_forward regexp l_string 0);
	let end_pos = Str.match_end () in
	String.sub l_string end_pos ((String.length l_string) - end_pos)
      with Not_found -> extract_element_name labels_tail raw_string regexp
    end
332

333 334 335 336 337 338 339 340 341 342
let get_element_name term raw_string  =
  let labels = Slab.elements term.t_label in
  let regexp = Str.regexp "model_trace:" in
  extract_element_name labels raw_string regexp


let rec build_model_rec raw_model terms model =
match raw_model with
  | [] -> model
  | model_element::raw_strings_tail ->
343
    let (element_name, element_location, element_term, terms_tail) =
344 345
      match terms with
      | [] -> (model_element.me_name, None, None, [])
346 347 348
      | term::t_tail ->
        ((get_element_name term model_element.me_name),
         term.t_loc,
349 350
         Some term, t_tail) in
    let new_model_element = create_model_element
351 352 353 354
      ~name:element_name
      ~value:model_element.me_value
      ?location:element_location
      ?term:element_term
355 356
      () in
    let model = add_to_model model new_model_element in
357 358 359
    build_model_rec
      raw_strings_tail
      terms_tail
360
      model
361

362 363 364 365 366

let build_model raw_model printer_mapping =
  build_model_rec raw_model printer_mapping.queried_terms empty_model


367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408
(*
***************************************************************
**  Filtering the model
***************************************************************
*)

let add_loc orig_model new_model position =
  (* Add a given location from orig_model to new_model *)

  let (file_name, line_num, _, _) = (Loc.get position) in
  let orig_model_file = get_model_file orig_model file_name in
  let new_model_file = get_model_file new_model file_name in

  if IntMap.mem line_num new_model_file then
    (* the location already is in new_model *)
    new_model
  else
    try
      (* get the location from original model *)
      let line_map = IntMap.find line_num orig_model_file in
      (* add the location to new model *)
      let new_model_file = IntMap.add line_num line_map new_model_file in
      StringMap.add file_name new_model_file new_model
    with Not_found ->
      new_model

let add_first_model_line filename model_file model =
  let (line_num, cnt_info) = IntMap.min_binding model_file in
  let mf = get_model_file model filename in
  let mf = IntMap.add line_num cnt_info mf in
  StringMap.add filename mf model

let model_for_positions_and_decls model ~positions =
  (* Start with empty model and add locations from model that
     are in locations *)
  let model_filtered = List.fold_left (add_loc model) empty_model positions in
  (* For each file add mapping corresponding to the first line of the
     counter-example from model to model_filtered.
     This corresponds to function declarations *)
  StringMap.fold add_first_model_line model model_filtered


409
(*
410
***************************************************************
411 412 413
** Registering model parser
***************************************************************
*)
414 415 416 417

exception KnownModelParser of string
exception UnknownModelParser of string

418 419 420 421 422 423 424 425 426
type reg_model_parser = Pp.formatted * raw_model_parser

let model_parsers : reg_model_parser Hstr.t = Hstr.create 17

let make_mp_from_raw (raw_mp:raw_model_parser) =
  fun input printer_mapping ->
    let raw_model = raw_mp input in
    build_model raw_model printer_mapping

427 428 429 430
let register_model_parser ~desc s p =
  if Hstr.mem model_parsers s then raise (KnownModelParser s);
  Hstr.replace model_parsers s (desc, p)

431
let lookup_raw_model_parser s =
432 433 434
  try snd (Hstr.find model_parsers s)
  with Not_found -> raise (UnknownModelParser s)

435 436 437
let lookup_model_parser s =
  make_mp_from_raw (lookup_raw_model_parser s)

438 439 440 441 442
let list_model_parsers () =
  Hstr.fold (fun k (desc,_) acc -> (k,desc)::acc) model_parsers []

let () = register_model_parser
  ~desc:"Model@ parser@ with@ no@ output@ (used@ if@ the@ solver@ does@ not@ support@ models." "no_model"
443
  (fun _ -> [])