model_parser.ml 24.5 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 12
(*                                                                  *)
(*  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 33 34 35 36
type float_type =
  | Plus_infinity
  | Minus_infinity
  | Plus_zero
  | Minus_zero
  | Not_a_number
  | Float_value of string * string * string
37
  | Float_hexa of string * float
38

39 40
type model_value =
 | Integer of string
41
 | Decimal of (string * string)
42
 | Fraction of (string * string)
43
 | Float of float_type
44
 | Boolean of bool
45
 | Array of model_array
46
 | Record of model_record
47
 | Bitvector of string
48
 | Apply of string * model_value list
49
 | Unparsed of string
50
and  arr_index = {
51
  arr_index_key : string; (* Even array indices can exceed MAX_INT with Z3 *)
52 53 54 55 56 57
  arr_index_value : model_value;
}
and model_array = {
  arr_others  : model_value;
  arr_indices : arr_index list;
}
58 59
and model_record = (field_name * model_value) list
and field_name = string
60 61 62 63 64 65 66 67

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

let array_add_element ~array ~index ~value =
68 69
  (*
     Adds the element value to the array on specified index.
70 71
  *)
  let arr_index = {
72
    arr_index_key = index;
73 74 75 76 77 78 79
    arr_index_value = value
  } in
  {
    arr_others = array.arr_others;
    arr_indices = arr_index::array.arr_indices;
  }

80 81 82
let convert_float_value f =
  match f with
  | Plus_infinity ->
83 84
      let m = Mstr.add "cons" (Json_base.String "Plus_infinity") Stdlib.Mstr.empty in
      Json_base.Record m
85
  | Minus_infinity ->
86 87
      let m = Mstr.add "cons" (Json_base.String "Minus_infinity") Stdlib.Mstr.empty in
      Json_base.Record m
88
  | Plus_zero ->
89 90
      let m = Mstr.add "cons" (Json_base.String "Plus_zero") Stdlib.Mstr.empty in
      Json_base.Record m
91
  | Minus_zero ->
92 93
      let m = Mstr.add "cons" (Json_base.String "Minus_zero") Stdlib.Mstr.empty in
      Json_base.Record m
94
  | Not_a_number ->
95 96
      let m = Mstr.add "cons" (Json_base.String "Not_a_number") Stdlib.Mstr.empty in
      Json_base.Record m
97
  | Float_value (b, eb, sb) ->
98 99 100 101 102
      let m = Mstr.add "cons" (Json_base.String "Float_value") Stdlib.Mstr.empty in
      let m = Mstr.add "sign" (Json_base.String b) m in
      let m = Mstr.add "exponent" (Json_base.String eb) m in
      let m = Mstr.add "significand" (Json_base.String sb) m in
      Json_base.Record m
103
  | Float_hexa(s,f) ->
104
      let m = Mstr.add "cons" (Json_base.String "Float_hexa") Stdlib.Mstr.empty in
105 106
      let m = Mstr.add "str_hexa" (Json_base.String s) m in
      let m = Mstr.add "value" (Json_base.Float f) m in
107
      Json_base.Record m
108

109
let rec convert_model_value value : Json_base.json =
110
  match value with
111
  | Integer s ->
112 113 114
      let m = Mstr.add "type" (Json_base.String "Integer") Stdlib.Mstr.empty in
      let m = Mstr.add "val" (Json_base.String s) m in
      Json_base.Record m
115
  | Float f ->
116
      let m = Mstr.add "type" (Json_base.String "Float") Stdlib.Mstr.empty in
117
      let m = Mstr.add "val" (convert_float_value f) m in
118
      Json_base.Record m
119
  | Decimal (int_part, fract_part) ->
120
      let m = Mstr.add "type" (Json_base.String "Decimal") Stdlib.Mstr.empty in
121 122
      let m = Mstr.add "val" (Json_base.String (int_part^"."^fract_part)) m in
      Json_base.Record m
123 124 125 126
  | Fraction (num, den) ->
      let m = Mstr.add "type" (Json_base.String "Fraction") Stdlib.Mstr.empty in
      let m = Mstr.add "val" (Json_base.String (num^"/"^den)) m in
      Json_base.Record m
127
  | Unparsed s ->
128 129 130
      let m = Mstr.add "type" (Json_base.String "Unparsed") Stdlib.Mstr.empty in
      let m = Mstr.add "val" (Json_base.String s) m in
      Json_base.Record m
131
  | Bitvector v ->
132 133 134
      let m = Mstr.add "type" (Json_base.String "Bv") Stdlib.Mstr.empty in
      let m = Mstr.add "val" (Json_base.String v) m in
      Json_base.Record m
135
  | Boolean b ->
136 137 138
      let m = Mstr.add "type" (Json_base.String "Boolean") Stdlib.Mstr.empty in
      let m = Mstr.add "val" (Json_base.Bool b) m in
      Json_base.Record m
139
  | Array a ->
140
      let l = convert_array a in
141 142 143
      let m = Mstr.add "type" (Json_base.String "Array") Stdlib.Mstr.empty in
      let m = Mstr.add "val" (Json_base.List l) m in
      Json_base.Record m
144 145 146 147 148 149 150 151 152 153
  | Apply (s, lt) ->
      let lt = List.map convert_model_value lt in
      let slt =
        let m = Mstr.add "list" (Json_base.List lt) Stdlib.Mstr.empty in
        let m = Mstr.add "apply" (Json_base.String s) m in
        Json_base.Record m
      in
      let m = Mstr.add "type" (Json_base.String "Apply") Stdlib.Mstr.empty in
      let m = Mstr.add "val" slt m in
      Json_base.Record m
154 155 156 157 158 159
  | Record r ->
      convert_record r

and convert_array a =
  let m_others =
    Mstr.add "others" (convert_model_value a.arr_others)  Stdlib.Mstr.empty in
160
  convert_indices a.arr_indices @ [Json_base.Record m_others]
161 162 163 164 165

and convert_indices indices =
  match indices with
  | [] -> []
  | index :: tail ->
166
    let m = Mstr.add "indice" (Json_base.String index.arr_index_key) Stdlib.Mstr.empty in
167
    let m = Mstr.add "value" (convert_model_value index.arr_index_value) m in
168
    Json_base.Record m :: convert_indices tail
169 170

and convert_record r =
171
  let m = Mstr.add "type" (Json_base.String "Record") Stdlib.Mstr.empty in
172 173 174
  let fields = convert_fields r in
  let m_field = Mstr.add "Field" fields Stdlib.Mstr.empty in
  let m = Mstr.add "val" (Json_base.Record m_field) m in
175
  Json_base.Record m
176 177

and convert_fields fields =
178 179 180 181 182 183 184
  Json_base.List
    (List.map
       (fun (f, v) ->
         let m = Mstr.add "field" (Json_base.String f) Stdlib.Mstr.empty in
         let m = Mstr.add "value" (convert_model_value v) m in
         Json_base.Record m)
       fields)
185 186 187

let print_model_value_sanit fmt v =
  let v = convert_model_value v in
188
  Json_base.print_json fmt v
189

190
let print_model_value = print_model_value_sanit
191

192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208

(******************************************)
(* Print values for humans                *)
(******************************************)
let print_float_human fmt f =
  match f with
  | Plus_infinity ->
      fprintf fmt "+∞"
  | Minus_infinity ->
      fprintf fmt "-∞"
  | Plus_zero ->
      fprintf fmt "+0"
  | Minus_zero ->
      fprintf fmt "-0"
  | Not_a_number ->
      fprintf fmt "NaN"
  | Float_value (b, eb, sb) ->
209
     fprintf fmt "float_bits(%s,%s,%s)" b eb sb
210
  | Float_hexa(s,f) -> fprintf fmt "%s (%g)" s f
211 212 213 214 215 216 217 218 219

let rec print_array_human fmt (arr: model_array) =
  fprintf fmt "(";
  List.iter (fun e ->
    fprintf fmt "%s => %a," e.arr_index_key print_model_value_human e.arr_index_value)
    arr.arr_indices;
  fprintf fmt "others => %a)" print_model_value_human arr.arr_others

and print_record_human fmt r =
220 221 222
  fprintf fmt "%a"
    (Pp.print_list_delim ~start:Pp.lbrace ~stop:Pp.rbrace ~sep:Pp.semi
    (fun fmt (f, v) -> fprintf fmt "%s = %a" f print_model_value_human v)) r
223 224 225 226 227

and print_model_value_human fmt (v: model_value) =
  match v with
  | Integer s -> fprintf fmt "%s" s
  | Decimal (s1,s2) -> fprintf fmt "%s" (s1 ^ "." ^ s2)
228
  | Fraction (s1, s2) -> fprintf fmt "%s" (s1 ^ "/" ^ s2)
229 230
  | Float f -> print_float_human fmt f
  | Boolean b -> fprintf fmt "%b"  b
231 232
  | Apply (s, lt) ->
    fprintf fmt "[%s %a]" s (Pp.print_list Pp.space print_model_value_human) lt
233 234 235 236 237
  | Array arr -> print_array_human fmt arr
  | Record r -> print_record_human fmt r
  | Bitvector s -> fprintf fmt "%s" s
  | Unparsed s -> fprintf fmt "%s" s

238
(*
239
***************************************************************
240 241 242
**  Model elements
***************************************************************
*)
243 244

type model_element_kind =
245 246
| Result
| Old
247
| Error_message
248 249
| Other

250 251 252 253 254
type model_element_name = {
  men_name   : string;
  men_kind   : model_element_kind;
}

255
type model_element = {
256
  me_name     : model_element_name;
257
  me_value    : model_value;
258 259
  me_location : Loc.position option;
  me_term     : Term.term option;
260
}
261

262
let split_model_trace_name mt_name =
263 264
  (* Mt_name is of the form "name[@type[@*]]". Return (name, type) *)
  let splitted = Strings.bounded_split '@' mt_name 3 in
265 266
  match splitted with
  | [first] -> (first, "")
267 268
  | first::second::_ -> (first, second)
  | [] -> ("", "")
269

270
let create_model_element ~name ~value ?location ?term () =
271
  let (name, type_s) = split_model_trace_name name in
272
  let me_kind = match type_s with
273 274 275
    | "result" -> Result
    | "old" -> Old
    | _ -> Other in
276 277 278 279
  let me_name = {
    men_name = name;
    men_kind = me_kind;
  } in
280
  {
281
    me_name = me_name;
282 283
    me_value = value;
    me_location = location;
284
    me_term = term;
285 286
  }

287 288 289 290 291 292 293 294
let construct_name (name: string): model_element_name =
  let (name, type_s) = split_model_trace_name name in
  let me_kind = match type_s with
  | "result" -> Result
  | "old" -> Old
  | _ -> Other in
  {men_name = name; men_kind = me_kind}

295
(*
296 297 298 299
let print_location fmt m_element =
    match m_element.me_location with
    | None -> fprintf fmt "\"no location\""
    | Some loc -> Loc.report_position fmt loc
300
*)
301 302

(*
303
***************************************************************
304 305
**  Model definitions
***************************************************************
306
*)
MARCHE Claude's avatar
MARCHE Claude committed
307 308
module IntMap = Stdlib.Mint
module StringMap = Stdlib.Mstr
309 310

type model_file = model_element list IntMap.t
311 312 313 314 315
type model_files = model_file StringMap.t
type model = {
  vc_term_loc : Loc.position option;
  model_files : model_files;
}
316 317 318

let empty_model = StringMap.empty
let empty_model_file = IntMap.empty
319 320 321 322 323 324
let is_model_empty model =
  model.model_files = empty_model
let default_model = {
  vc_term_loc = None;
  model_files = empty_model;
}
325 326 327

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

328 329 330
type raw_model_parser =
  Stdlib.Sstr.t -> ((string * string) list) Stdlib.Mstr.t ->
    string -> model_element list
331 332

(*
333
***************************************************************
334 335 336
**  Quering the model
***************************************************************
*)
337
let print_model_element print_model_value me_name_trans fmt m_element =
338 339
  match m_element.me_name.men_kind with
  | Error_message ->
340
    fprintf fmt "%s" m_element.me_name.men_name
341
  | _ ->
342
    let me_name = me_name_trans m_element.me_name in
343
    fprintf fmt  "%s = %a"
344
      me_name print_model_value m_element.me_value
345

346 347
let print_model_elements ?(sep = "\n") print_model_value me_name_trans fmt m_elements =
  Pp.print_list (fun fmt () -> Pp.string fmt sep) (print_model_element print_model_value me_name_trans) fmt m_elements
348

349
let print_model_file ~print_model_value fmt me_name_trans filename model_file =
MARCHE Claude's avatar
MARCHE Claude committed
350
  (* Relativize does not work on nighly bench: using basename instead. It
351
     hides the local paths.  *)
MARCHE Claude's avatar
MARCHE Claude committed
352
  let filename = Filename.basename filename  in
353
  fprintf fmt "File %s:" filename;
354
  IntMap.iter
355
    (fun line m_elements ->
356
      fprintf fmt "@\nLine %d:@\n" line;
357
      print_model_elements print_model_value me_name_trans fmt m_elements)
358 359
    model_file;
  fprintf fmt "@\n"
360

361 362
let why_name_trans me_name =
  match me_name.men_kind with
363
  | Result -> "result"
364
  | Old    -> "old" ^ " " ^ me_name.men_name
365
  | _  -> me_name.men_name
366 367 368

let print_model
    ?(me_name_trans = why_name_trans)
369
    ~print_model_value
370
    fmt
371
    model =
MARCHE Claude's avatar
MARCHE Claude committed
372 373 374
  (* Simple and easy way to print file sorted alphabetically
   FIXME: but StringMap.iter is supposed to iter in alphabetic order, so waste of time and memory here !
   *)
375
  let l = StringMap.bindings model.model_files in
376 377 378 379 380 381 382 383 384 385 386
  List.iter (fun (k, e) -> print_model_file ~print_model_value fmt me_name_trans k e) l

let print_model_human
    ?(me_name_trans = why_name_trans)
    fmt
    model = print_model ~me_name_trans ~print_model_value:print_model_value_human fmt model


let print_model ?(me_name_trans = why_name_trans)
    fmt
    model = print_model ~me_name_trans ~print_model_value fmt model
387

388 389 390
let model_to_string
    ?(me_name_trans = why_name_trans)
    model =
391
  print_model ~me_name_trans str_formatter model;
392 393
  flush_str_formatter ()

394 395 396 397 398
let get_model_file model filename =
  try
    StringMap.find filename model
  with Not_found ->
    empty_model_file
399

400 401 402 403 404
let get_elements model_file line_number =
  try
    IntMap.find line_number model_file
  with Not_found ->
    []
405

406 407 408 409 410
let print_model_vc_term
    ?(me_name_trans = why_name_trans)
    ?(sep = "\n")
    fmt
    model =
411 412 413 414 415 416 417
  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
418
      print_model_elements ~sep print_model_value me_name_trans fmt model_elements
419

420 421 422 423 424 425 426
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 ()

427
let get_padding line =
428
  try
429 430 431 432 433
    let r = Str.regexp " *" in
    ignore (Str.search_forward r line 0);
    Str.matched_string line
  with Not_found -> ""

434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459
(* This assumes that l is sorted and split the list of locations in two:
   those that are applied on this line and the others. For those that are on
   this line, we split the locations that appear on several lines. *)
let rec partition_loc line lc l =
  match l with
  | (hd,a) :: tl ->
      let (hdf, hdl, hdfc, hdlc) = Loc.get hd in
      if hdl = line then
        if hdlc > lc then
          let old_sloc = Loc.user_position hdf hdl hdfc lc in
          let newlc = hdlc - lc in
          let new_sloc = Loc.user_position hdf (hdl + 1) 1 newlc in
          let (rem_loc, new_loc) = partition_loc line lc tl in
          ((new_sloc,a) :: rem_loc, (old_sloc,a) :: new_loc)
        else
          let (rem_loc, new_loc) = partition_loc line lc tl in
          (rem_loc, (hd,a) :: new_loc)
      else
        (l, [])
  | _ -> (l, [])

(* Change a locations so that it points to a different line number *)
let add_offset off (loc, a) =
  let (f, l, fc, lc) = Loc.get loc in
  (Loc.user_position f (l + off) fc lc, a)

460 461 462 463 464
let interleave_line
    start_comment
    end_comment
    me_name_trans
    model_file
465
    (source_code, line_number, offset, remaining_locs, locs)
466
    line =
467 468 469 470
  let remaining_locs, list_loc =
    partition_loc line_number (String.length line) remaining_locs
  in
  let list_loc = List.map (add_offset offset) list_loc in
471 472
  try
    let model_elements = IntMap.find line_number model_file in
473
    print_model_elements print_model_value_human me_name_trans str_formatter model_elements ~sep:"; ";
474
    let cntexmp_line =
475 476
     (get_padding line) ^ start_comment ^ (flush_str_formatter ()) ^ end_comment
    in
477

478 479 480 481 482 483 484
    (* We need to know how many lines will be taken by the counterexample. This
       is ad hoc as we don't really know how the lines are split in IDE. *)
    let len_cnt =
      1 + (String.length cntexmp_line) / 80
    in

    (source_code ^ line ^ cntexmp_line ^ "\n", line_number + 1, offset + len_cnt, remaining_locs, list_loc @ locs)
485
  with Not_found ->
486
    (source_code ^ line, line_number + 1, offset, remaining_locs, list_loc @ locs)
487

488 489 490 491

let interleave_with_source
    ?(start_comment="(* ")
    ?(end_comment=" *)")
492
    ?(me_name_trans = why_name_trans)
493
    model
494 495 496 497 498 499 500
    ~rel_filename
    ~source_code
    ~locations =
  let locations =
    List.sort (fun x y -> compare (fst x) (fst y))
      (List.filter (fun x -> let (f, _, _, _) = Loc.get (fst x) in f = rel_filename) locations)
  in
501
  try
502 503 504 505 506 507 508 509 510
    (* There is no way to compare rel_filename and the locations of filename in
       the file because they contain extra ".." which cannot be reliably removed
       (because of potential symbolic link). So, we use the basename.
    *)
    let model_files =
      StringMap.filter (fun k _ -> Filename.basename k = Filename.basename rel_filename)
        model.model_files
    in
    let model_file = snd (StringMap.choose model_files) in
511 512
    let src_lines_up_to_last_cntexmp_el source_code model_file =
      let (last_cntexmp_line, _) = IntMap.max_binding model_file in
513 514
      Str.bounded_split (Str.regexp "^") source_code (last_cntexmp_line+1)
    in
515 516 517 518 519 520 521 522
    let (source_code, _, _, _, gen_loc) =
      List.fold_left
        (interleave_line
           start_comment end_comment me_name_trans model_file)
        ("", 1, 0, locations, [])
        (src_lines_up_to_last_cntexmp_el source_code model_file)
    in
    source_code, gen_loc
523
  with Not_found ->
524
    source_code, locations
525 526 527 528 529


(*
**  Quering the model - json
*)
530 531
let print_model_element_json me_name_to_str fmt me =
  let print_value fmt =
532
    fprintf fmt "%a" print_model_value_sanit me.me_value in
533 534
  let print_kind fmt =
    match me.me_name.men_kind with
535 536 537 538
    | Result -> fprintf fmt "%a" Json_base.string "result"
    | Old -> fprintf fmt "%a" Json_base.string "old"
    | Error_message -> fprintf fmt "%a" Json_base.string "error_message"
    | Other -> fprintf fmt "%a" Json_base.string "other" in
539
  let print_name fmt =
540
    Json_base.string fmt (me_name_to_str me) in
541 542
  let print_value_or_kind_or_name fmt printer =
    printer fmt in
543
  Json_base.map_bindings
544 545 546 547 548 549
    (fun s -> s)
    print_value_or_kind_or_name
    fmt
    [("name", print_name);
     ("value", print_value);
     ("kind", print_kind)]
550

551
let print_model_elements_json me_name_to_str fmt model_elements =
552
  Json_base.list
553
    (print_model_element_json me_name_to_str)
554
    fmt
555
    model_elements
556

557 558
let print_model_elements_on_lines_json model me_name_to_str vc_line_trans fmt
    (file_name, model_file) =
559
  Json_base.map_bindings
560 561 562 563 564 565 566 567 568 569 570
    (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
    )
571
    (print_model_elements_json me_name_to_str)
572 573
    fmt
    (IntMap.bindings model_file)
574

575 576
let print_model_json
    ?(me_name_trans = why_name_trans)
577
    ?(vc_line_trans = (fun i -> string_of_int i))
578
    fmt
579
    model =
580
  let me_name_to_str = fun me ->
581
    me_name_trans me.me_name in
582 583 584 585 586
  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
587
  Json_base.map_bindings
588
    (fun s -> s)
589
    (print_model_elements_on_lines_json model me_name_to_str vc_line_trans)
590
    fmt
591
    model_files_bindings
592

593

594 595
let model_to_string_json
    ?(me_name_trans = why_name_trans)
596
    ?(vc_line_trans = (fun i -> string_of_int i))
597
    model =
598
  print_model_json str_formatter ~me_name_trans ~vc_line_trans model;
599
  flush_str_formatter ()
600

601

602
(*
603
***************************************************************
604 605 606 607 608 609 610 611 612 613 614 615 616 617 618
**  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

619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636
let build_model_rec (raw_model: model_element list) (term_map: Term.term Mstr.t) (model: model_files) =
  List.fold_left (fun model raw_element ->
    let raw_element_name = raw_element.me_name.men_name in
    try
      (
       let t = Mstr.find raw_element_name term_map in
       let real_model_trace = construct_name (get_model_trace_string ~labels:t.t_label) in
       let model_element = {
	 me_name = real_model_trace;
	 me_value = raw_element.me_value;
	 me_location = t.t_loc;
	 me_term = Some t;
       } in
       add_to_model model model_element
      )
    with Not_found -> model)
    model
    raw_model
637

638 639
let handle_contradictory_vc model_files vc_term_loc =
  (* The VC is contradictory if the location of the term that triggers VC
640 641
     was collected, model_files is not empty, and there are no model elements
     in this location.
642 643
     If this is the case, add model element saying that VC is contradictory
     to this location. *)
644 645 646 647 648 649 650 651 652 653 654 655 656
  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  *)
657 658
	let me_name = {
	  men_name = "the check fails with all inputs";
659
	  men_kind = Error_message;
660
	} in
661
	let me = {
662
	  me_name = me_name;
663 664 665 666 667 668 669
	  me_value = Unparsed "";
	  me_location = Some pos;
	  me_term = None;
	} in
	add_to_model model_files me
      else
	model_files
670

671
let build_model raw_model printer_mapping =
672
  let model_files = build_model_rec raw_model printer_mapping.queried_terms empty_model in
673
  let model_files = handle_contradictory_vc model_files printer_mapping.Printer.vc_term_loc in
674 675 676 677
  {
    vc_term_loc = printer_mapping.Printer.vc_term_loc;
    model_files = model_files;
  }
678 679


680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714
(*
***************************************************************
**  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 *)
715
  let model_filtered = List.fold_left (add_loc model.model_files) empty_model positions in
716 717 718
  (* For each file add mapping corresponding to the first line of the
     counter-example from model to model_filtered.
     This corresponds to function declarations *)
719 720 721
  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 }
722 723


724
(*
725
***************************************************************
726 727 728
** Registering model parser
***************************************************************
*)
729 730 731 732

exception KnownModelParser of string
exception UnknownModelParser of string

733 734 735 736 737 738
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 ->
739
    let list_proj = printer_mapping.list_projections in
740 741
    let list_records = printer_mapping.list_records in
    let raw_model = raw_mp list_proj list_records input in
742 743
    build_model raw_model printer_mapping

744 745 746 747
let register_model_parser ~desc s p =
  if Hstr.mem model_parsers s then raise (KnownModelParser s);
  Hstr.replace model_parsers s (desc, p)

748
let lookup_raw_model_parser s : raw_model_parser =
749 750 751
  try snd (Hstr.find model_parsers s)
  with Not_found -> raise (UnknownModelParser s)

752
let lookup_model_parser s : model_parser =
753 754
  make_mp_from_raw (lookup_raw_model_parser s)

755 756 757 758 759
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"
760
  (fun _ _ _ -> [])