model_parser.ml 15 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
 | Bitvector of int
34
 | Unparsed of string
35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50
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 =
51 52
  (*
     Adds the element value to the array on specified index.
53 54 55 56 57 58 59 60 61 62 63 64 65
  *)
  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;
  }

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

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

91 92

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

102
type model_element = {
103
  me_name     : string;
104
  me_type     : model_element_type;
105
  me_value    : model_value;
106 107
  me_location : Loc.position option;
  me_term     : Term.term option;
108
  me_text_info: bool;
109
}
110

111 112 113 114 115 116 117 118 119
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 [] *)
    ("", "")

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

135
(*
136 137 138 139
let print_location fmt m_element =
    match m_element.me_location with
    | None -> fprintf fmt "\"no location\""
    | Some loc -> Loc.report_position fmt loc
140
*)
141 142

(*
143
***************************************************************
144 145
**  Model definitions
***************************************************************
146
*)
147 148 149 150
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
151 152 153 154 155
type model_files = model_file StringMap.t
type model = {
  vc_term_loc : Loc.position option;
  model_files : model_files;
}
156 157 158

let empty_model = StringMap.empty
let empty_model_file = IntMap.empty
159 160 161 162 163 164
let is_model_empty model =
  model.model_files = empty_model
let default_model = {
  vc_term_loc = None;
  model_files = empty_model;
}
165 166 167 168 169 170

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

type raw_model_parser =  string -> model_element list

(*
171
***************************************************************
172 173 174
**  Quering the model
***************************************************************
*)
175
let print_model_element me_name_trans fmt m_element =
176 177 178 179 180
  if m_element.me_text_info then
    fprintf fmt "%s" m_element.me_name
  else
    let me_name = me_name_trans (m_element.me_name, m_element.me_type) in
    fprintf fmt  "%s = %a"
181
      me_name print_model_value m_element.me_value
182

183 184
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
185

186 187
let print_model_file fmt me_name_trans filename model_file =
  fprintf fmt "File %s:" filename;
188
  IntMap.iter
189
    (fun line m_elements ->
190 191
      fprintf fmt "\nLine %d:\n" line;
      print_model_elements me_name_trans fmt m_elements)
192
    model_file
193

194 195 196 197 198 199 200 201 202
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
203
    model =
204
  StringMap.iter (print_model_file fmt me_name_trans) model.model_files
205

206 207 208
let model_to_string
    ?(me_name_trans = why_name_trans)
    model =
209
  print_model ~me_name_trans str_formatter model;
210 211
  flush_str_formatter ()

212 213 214 215 216
let get_model_file model filename =
  try
    StringMap.find filename model
  with Not_found ->
    empty_model_file
217

218 219 220 221 222
let get_elements model_file line_number =
  try
    IntMap.find line_number model_file
  with Not_found ->
    []
223

224 225 226 227 228
let print_model_vc_term
    ?(me_name_trans = why_name_trans)
    ?(sep = "\n")
    fmt
    model =
229 230 231 232 233 234 235 236
  if not (is_model_empty model) then
    match model.vc_term_loc with
    | None -> fprintf fmt "error: cannot get location of the check"
    | Some pos ->
      let (filename, line_number, _, _) = Loc.get pos in
      let model_file = get_model_file model.model_files filename in
      let model_elements = get_elements model_file line_number in
      print_model_elements ~sep me_name_trans fmt model_elements
237

238 239 240 241 242 243 244
let model_vc_term_to_string
    ?(me_name_trans = why_name_trans)
    ?(sep = "\n")
    model =
  print_model_vc_term ~me_name_trans ~sep str_formatter model;
  flush_str_formatter ()

245
let get_padding line =
246
  try
247 248 249 250 251
    let r = Str.regexp " *" in
    ignore (Str.search_forward r line 0);
    Str.matched_string line
  with Not_found -> ""

252 253 254 255 256 257 258
let interleave_line
    start_comment
    end_comment
    me_name_trans
    model_file
    (source_code, line_number)
    line =
259 260
  try
    let model_elements = IntMap.find line_number model_file in
261
    print_model_elements me_name_trans str_formatter model_elements ~sep:"; ";
262
    let cntexmp_line =
263
      (get_padding line) ^
264 265
	start_comment ^
	(flush_str_formatter ()) ^
266
	end_comment in
267

268
    (source_code ^ line ^ cntexmp_line ^ "\n", line_number + 1)
269 270 271
  with Not_found ->
    (source_code ^ line, line_number + 1)

272 273 274 275

let interleave_with_source
    ?(start_comment="(* ")
    ?(end_comment=" *)")
276
    ?(me_name_trans = why_name_trans)
277
    model
278 279
    ~filename
    ~source_code =
280
  try
281
    let model_file = StringMap.find  filename model.model_files in
282 283
    let lines = Str.split (Str.regexp "^") source_code in
    let (source_code, _) = List.fold_left
284 285
      (interleave_line
	 start_comment end_comment me_name_trans model_file)
286 287
      ("", 1)
      lines in
288 289 290
    source_code
  with Not_found ->
    source_code
291 292 293 294 295


(*
**  Quering the model - json
*)
296
let print_model_value_json fmt me_value =
297 298
  fprintf fmt "%a" (print_model_value_sanit Json.string) me_value

299
let model_elements_to_map_bindings model_elements =
300
  List.fold_left
301
    (fun map_bindings me ->
302
      List.append map_bindings [(me, me.me_value)]
303
    )
304
    []
305 306
    model_elements

307
let print_model_elements_json me_name_to_str fmt model_elements =
308
  Json.map_bindings
309
    me_name_to_str
310 311 312
    print_model_value_json
    fmt
    (model_elements_to_map_bindings model_elements)
313

314
let print_model_elements_on_lines_json me_name_to_str fmt model_file =
315 316
  Json.map_bindings
    (fun i -> string_of_int i)
317
    (print_model_elements_json me_name_to_str)
318 319
    fmt
    (IntMap.bindings model_file)
320

321 322 323
let print_model_json
    ?(me_name_trans = why_name_trans)
    fmt
324
    model =
325 326
  let me_name_to_str = fun me ->
    me_name_trans (me.me_name, me.me_type) in
327 328
  Json.map_bindings
    (fun s -> s)
329
    (print_model_elements_on_lines_json me_name_to_str)
330
    fmt
331
    (StringMap.bindings model.model_files)
332

333 334 335
let model_to_string_json
    ?(me_name_trans = why_name_trans)
    model =
336
  print_model_json str_formatter ~me_name_trans model;
337
  flush_str_formatter ()
338

339

340
(*
341
***************************************************************
342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362
**  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
363 364
    begin
      try
365 366 367 368 369
	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
370

371 372 373 374 375 376 377 378 379 380
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 ->
381
    let (element_name, element_location, element_term, terms_tail) =
382 383
      match terms with
      | [] -> (model_element.me_name, None, None, [])
384 385 386
      | term::t_tail ->
        ((get_element_name term model_element.me_name),
         term.t_loc,
387 388
         Some term, t_tail) in
    let new_model_element = create_model_element
389 390 391 392
      ~name:element_name
      ~value:model_element.me_value
      ?location:element_location
      ?term:element_term
393 394
      () in
    let model = add_to_model model new_model_element in
395 396 397
    build_model_rec
      raw_strings_tail
      terms_tail
398
      model
399

400 401
let handle_contradictory_vc model_files vc_term_loc =
  (* The VC is contradictory if the location of the term that triggers VC
402 403
     was collected, model_files is not empty, and there are no model elements
     in this location.
404 405
     If this is the case, add model element saying that VC is contradictory
     to this location. *)
406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429
  if model_files = empty_model then
    (* If the counterexample model was not collected, then model_files
       is empty and this does not mean that VC is contradictory. *)
    model_files
  else
    match vc_term_loc with
    | None -> model_files
    | Some pos ->
      let (filename, line_number, _, _) = Loc.get pos in
      let model_file = get_model_file model_files filename in
      let model_elements = get_elements model_file line_number in
      if model_elements = [] then
      (* The vc is contradictory, add special model element  *)
	let me = {
	  me_name = "the check fails with all inputs";
	  me_type = Other;
	  me_value = Unparsed "";
	  me_location = Some pos;
	  me_term = None;
	  me_text_info = true;
	} in
	add_to_model model_files me
      else
	model_files
430

431
let build_model raw_model printer_mapping =
432
  let model_files = build_model_rec raw_model printer_mapping.queried_terms empty_model in
433
  let model_files = handle_contradictory_vc model_files printer_mapping.Printer.vc_term_loc in
434 435 436 437
  {
    vc_term_loc = printer_mapping.Printer.vc_term_loc;
    model_files = model_files;
  }
438 439


440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474
(*
***************************************************************
**  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 *)
475
  let model_filtered = List.fold_left (add_loc model.model_files) empty_model positions in
476 477 478
  (* For each file add mapping corresponding to the first line of the
     counter-example from model to model_filtered.
     This corresponds to function declarations *)
479 480 481
  let model_filtered = StringMap.fold add_first_model_line model.model_files model_filtered in
  { vc_term_loc = model.vc_term_loc;
    model_files = model_filtered }
482 483


484
(*
485
***************************************************************
486 487 488
** Registering model parser
***************************************************************
*)
489 490 491 492

exception KnownModelParser of string
exception UnknownModelParser of string

493 494 495 496 497 498 499 500 501
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

502 503 504 505
let register_model_parser ~desc s p =
  if Hstr.mem model_parsers s then raise (KnownModelParser s);
  Hstr.replace model_parsers s (desc, p)

506
let lookup_raw_model_parser s =
507 508 509
  try snd (Hstr.find model_parsers s)
  with Not_found -> raise (UnknownModelParser s)

510 511 512
let lookup_model_parser s =
  make_mp_from_raw (lookup_raw_model_parser s)

513 514 515 516 517
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"
518
  (fun _ -> [])