model_parser.ml 16.1 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

type model_value =
 | Integer of string
32
 | Decimal of (string * string)
33
 | Array of model_array
34
 | Bitvector of string
35
 | Unparsed of string
36
and  arr_index = {
37
  arr_index_key : model_value;
38 39 40 41 42 43 44 45 46 47 48 49 50 51
  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 =
52 53
  (*
     Adds the element value to the array on specified index.
54 55
  *)
  let arr_index = {
56
    arr_index_key = index;
57 58 59 60 61 62 63
    arr_index_value = value
  } in
  {
    arr_others = array.arr_others;
    arr_indices = arr_index::array.arr_indices;
  }

64
let rec print_indices fmt indices =
65 66 67
  match indices with
  | [] -> ()
  | index::tail ->
68
    fprintf fmt "%a => " print_model_value index.arr_index_key;
69
    print_model_value fmt index.arr_index_value;
70
    fprintf fmt ", ";
71
    print_indices fmt tail
72
and
73
print_array fmt arr =
74
  fprintf fmt "(";
75
  print_indices fmt arr.arr_indices;
76 77
  fprintf fmt "others => ";
  print_model_value fmt arr.arr_others;
78
  fprintf fmt ")"
79
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
  | Decimal (int_part, fract_part) ->
85
    sanit_print fmt (int_part^"."^fract_part)
86
  | Unparsed s -> sanit_print fmt s
87 88
  | Array a ->
    print_array str_formatter a;
89
    sanit_print fmt (flush_str_formatter ())
90
  | Bitvector v -> sanit_print fmt v
91 92
and
print_model_value fmt value =
93
  print_model_value_sanit (fun fmt s -> fprintf fmt "%s" s) fmt value
94

95 96

(*
97
***************************************************************
98 99 100
**  Model elements
***************************************************************
*)
101 102

type model_element_kind =
103 104
| Result
| Old
105
| Error_message
106 107
| Other

108 109 110 111 112
type model_element_name = {
  men_name   : string;
  men_kind   : model_element_kind;
}

113
type model_element = {
114
  me_name     : model_element_name;
115
  me_value    : model_value;
116 117
  me_location : Loc.position option;
  me_term     : Term.term option;
118
}
119

120
let split_model_trace_name mt_name =
121 122
  (* Mt_name is of the form "name[@type[@*]]". Return (name, type) *)
  let splitted = Strings.bounded_split '@' mt_name 3 in
123 124
  match splitted with
  | [first] -> (first, "")
125 126
  | first::second::_ -> (first, second)
  | [] -> ("", "")
127

128
let create_model_element ~name ~value ?location ?term () =
129
  let (name, type_s) = split_model_trace_name name in
130
  let me_kind = match type_s with
131 132 133
    | "result" -> Result
    | "old" -> Old
    | _ -> Other in
134 135 136 137
  let me_name = {
    men_name = name;
    men_kind = me_kind;
  } in
138
  {
139
    me_name = me_name;
140 141
    me_value = value;
    me_location = location;
142
    me_term = term;
143 144
  }

145
(*
146 147 148 149
let print_location fmt m_element =
    match m_element.me_location with
    | None -> fprintf fmt "\"no location\""
    | Some loc -> Loc.report_position fmt loc
150
*)
151 152

(*
153
***************************************************************
154 155
**  Model definitions
***************************************************************
156
*)
157 158 159 160
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
161 162 163 164 165
type model_files = model_file StringMap.t
type model = {
  vc_term_loc : Loc.position option;
  model_files : model_files;
}
166 167 168

let empty_model = StringMap.empty
let empty_model_file = IntMap.empty
169 170 171 172 173 174
let is_model_empty model =
  model.model_files = empty_model
let default_model = {
  vc_term_loc = None;
  model_files = empty_model;
}
175 176 177 178 179 180

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

type raw_model_parser =  string -> model_element list

(*
181
***************************************************************
182 183 184
**  Quering the model
***************************************************************
*)
185
let print_model_element me_name_trans fmt m_element =
186 187
  match m_element.me_name.men_kind with
  | Error_message ->
188
    fprintf fmt "%s" m_element.me_name.men_name
189
  | _ ->
190
    let me_name = me_name_trans m_element.me_name in
191
    fprintf fmt  "%s = %a"
192
      me_name print_model_value m_element.me_value
193

194 195
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
196

197 198
let print_model_file fmt me_name_trans filename model_file =
  fprintf fmt "File %s:" filename;
199
  IntMap.iter
200
    (fun line m_elements ->
201 202
      fprintf fmt "\nLine %d:\n" line;
      print_model_elements me_name_trans fmt m_elements)
203
    model_file
204

205 206
let why_name_trans me_name =
  match me_name.men_kind with
207
  | Result -> "result"
208
  | Old    -> "old" ^ " " ^ me_name.men_name
209
  | _  -> me_name.men_name
210 211 212 213

let print_model
    ?(me_name_trans = why_name_trans)
    fmt
214
    model =
215
  StringMap.iter (print_model_file fmt me_name_trans) model.model_files
216

217 218 219
let model_to_string
    ?(me_name_trans = why_name_trans)
    model =
220
  print_model ~me_name_trans str_formatter model;
221 222
  flush_str_formatter ()

223 224 225 226 227
let get_model_file model filename =
  try
    StringMap.find filename model
  with Not_found ->
    empty_model_file
228

229 230 231 232 233
let get_elements model_file line_number =
  try
    IntMap.find line_number model_file
  with Not_found ->
    []
234

235 236 237 238 239
let print_model_vc_term
    ?(me_name_trans = why_name_trans)
    ?(sep = "\n")
    fmt
    model =
240 241 242 243 244 245 246 247
  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
248

249 250 251 252 253 254 255
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 ()

256
let get_padding line =
257
  try
258 259 260 261 262
    let r = Str.regexp " *" in
    ignore (Str.search_forward r line 0);
    Str.matched_string line
  with Not_found -> ""

263 264 265 266 267 268 269
let interleave_line
    start_comment
    end_comment
    me_name_trans
    model_file
    (source_code, line_number)
    line =
270 271
  try
    let model_elements = IntMap.find line_number model_file in
272
    print_model_elements me_name_trans str_formatter model_elements ~sep:"; ";
273
    let cntexmp_line =
274
      (get_padding line) ^
275 276
	start_comment ^
	(flush_str_formatter ()) ^
277
	end_comment in
278

279
    (source_code ^ line ^ cntexmp_line ^ "\n", line_number + 1)
280 281 282
  with Not_found ->
    (source_code ^ line, line_number + 1)

283 284 285 286

let interleave_with_source
    ?(start_comment="(* ")
    ?(end_comment=" *)")
287
    ?(me_name_trans = why_name_trans)
288
    model
289 290
    ~filename
    ~source_code =
291
  try
292 293 294 295 296 297 298 299 300 301 302
    let model_file = StringMap.find filename model.model_files in
    let src_lines_up_to_last_cntexmp_el source_code model_file =
      let (last_cntexmp_line, _) = IntMap.max_binding model_file in
      let lines = Str.bounded_split (Str.regexp "^") source_code (last_cntexmp_line+1) in
      let remove_last_element list =
	let list_rev = List.rev list in
	match list_rev with
	| _ :: tail -> List.rev tail
	| _ -> List.rev list_rev
      in
      remove_last_element lines in
303
    let (source_code, _) = List.fold_left
304 305
      (interleave_line
	 start_comment end_comment me_name_trans model_file)
306
      ("", 1)
307
      (src_lines_up_to_last_cntexmp_el source_code model_file) in
308 309 310
    source_code
  with Not_found ->
    source_code
311 312 313 314 315


(*
**  Quering the model - json
*)
316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335
let print_model_element_json me_name_to_str fmt me =
  let print_value fmt =
    fprintf fmt "%a" (print_model_value_sanit Json.string) me.me_value in
  let print_kind fmt =
    match me.me_name.men_kind with
    | Result -> fprintf fmt "%a" Json.string "result"
    | Old -> fprintf fmt "%a" Json.string "old"
    | Error_message -> fprintf fmt "%a" Json.string "error_message"
    | Other -> fprintf fmt "%a" Json.string "other" in
  let print_name fmt =
    Json.string fmt (me_name_to_str me) in
  let print_value_or_kind_or_name fmt printer =
    printer fmt in
  Json.map_bindings
    (fun s -> s)
    print_value_or_kind_or_name
    fmt
    [("name", print_name);
     ("value", print_value);
     ("kind", print_kind)]
336

337
let print_model_elements_json me_name_to_str fmt model_elements =
338 339
  Json.list
    (print_model_element_json me_name_to_str)
340
    fmt
341
    model_elements
342

343 344
let print_model_elements_on_lines_json model me_name_to_str vc_line_trans fmt
    (file_name, model_file) =
345
  Json.map_bindings
346 347 348 349 350 351 352 353 354 355 356
    (fun i ->
      match model.vc_term_loc with
      | None ->
	string_of_int i
      | Some pos ->
	let (vc_file_name, line, _, _) = Loc.get pos in
	if file_name = vc_file_name && i = line then
	  vc_line_trans i
	else
	  string_of_int i
    )
357
    (print_model_elements_json me_name_to_str)
358 359
    fmt
    (IntMap.bindings model_file)
360

361 362
let print_model_json
    ?(me_name_trans = why_name_trans)
363
    ?(vc_line_trans = (fun i -> string_of_int i))
364
    fmt
365
    model =
366
  let me_name_to_str = fun me ->
367
    me_name_trans me.me_name in
368 369 370 371 372
  let model_files_bindings = List.fold_left
    (fun bindings (file_name, model_file) ->
      List.append bindings [(file_name, (file_name, model_file))])
    []
    (StringMap.bindings model.model_files) in
373 374
  Json.map_bindings
    (fun s -> s)
375
    (print_model_elements_on_lines_json model me_name_to_str vc_line_trans)
376
    fmt
377
    model_files_bindings
378

379 380
let model_to_string_json
    ?(me_name_trans = why_name_trans)
381
    ?(vc_line_trans = (fun i -> string_of_int i))
382
    model =
383
  print_model_json str_formatter ~me_name_trans ~vc_line_trans model;
384
  flush_str_formatter ()
385

386

387
(*
388
***************************************************************
389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407
**  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

let rec build_model_rec raw_model terms model =
match raw_model with
  | [] -> model
  | model_element::raw_strings_tail ->
408
    let (element_name, element_location, element_term, terms_tail) =
409
      match terms with
410
      | [] -> (model_element.me_name.men_name, None, None, [])
411
      | term::t_tail ->
412 413 414 415
	let get_element_name term raw_string  =
	  try
	    get_model_trace_string ~labels:term.t_label
	  with Not_found -> raw_string in
416
        ((get_element_name term model_element.me_name.men_name),
417
         term.t_loc,
418 419
         Some term, t_tail) in
    let new_model_element = create_model_element
420 421 422 423
      ~name:element_name
      ~value:model_element.me_value
      ?location:element_location
      ?term:element_term
424 425
      () in
    let model = add_to_model model new_model_element in
426 427 428
    build_model_rec
      raw_strings_tail
      terms_tail
429
      model
430

431 432
let handle_contradictory_vc model_files vc_term_loc =
  (* The VC is contradictory if the location of the term that triggers VC
433 434
     was collected, model_files is not empty, and there are no model elements
     in this location.
435 436
     If this is the case, add model element saying that VC is contradictory
     to this location. *)
437 438 439 440 441 442 443 444 445 446 447 448 449
  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  *)
450 451
	let me_name = {
	  men_name = "the check fails with all inputs";
452
	  men_kind = Error_message;
453
	} in
454
	let me = {
455
	  me_name = me_name;
456 457 458 459 460 461 462
	  me_value = Unparsed "";
	  me_location = Some pos;
	  me_term = None;
	} in
	add_to_model model_files me
      else
	model_files
463

464
let build_model raw_model printer_mapping =
465
  let model_files = build_model_rec raw_model printer_mapping.queried_terms empty_model in
466
  let model_files = handle_contradictory_vc model_files printer_mapping.Printer.vc_term_loc in
467 468 469 470
  {
    vc_term_loc = printer_mapping.Printer.vc_term_loc;
    model_files = model_files;
  }
471 472


473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507
(*
***************************************************************
**  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 *)
508
  let model_filtered = List.fold_left (add_loc model.model_files) empty_model positions in
509 510 511
  (* For each file add mapping corresponding to the first line of the
     counter-example from model to model_filtered.
     This corresponds to function declarations *)
512 513 514
  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 }
515 516


517
(*
518
***************************************************************
519 520 521
** Registering model parser
***************************************************************
*)
522 523 524 525

exception KnownModelParser of string
exception UnknownModelParser of string

526 527 528 529 530 531 532 533 534
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

535 536 537 538
let register_model_parser ~desc s p =
  if Hstr.mem model_parsers s then raise (KnownModelParser s);
  Hstr.replace model_parsers s (desc, p)

539
let lookup_raw_model_parser s =
540 541 542
  try snd (Hstr.find model_parsers s)
  with Not_found -> raise (UnknownModelParser s)

543 544 545
let lookup_model_parser s =
  make_mp_from_raw (lookup_raw_model_parser s)

546 547 548 549 550
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"
551
  (fun _ -> [])