model_parser.ml 29.6 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
open Wstdlib
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
let interp_float ?(interp=true) b eb sb =
41
    try
42 43 44
      (* We don't interpret when this is disable *)
      if not interp then
        raise Exit;
45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94
      let is_neg = match b with
        | "#b0" -> false
        | "#b1" -> true
        | _ -> raise Exit
      in
      if String.length eb = 13 && String.sub eb 0 2 = "#b" &&
         String.length sb = 15 && String.sub sb 0 2 = "#x" then
         (* binary 64 *)
         let exp_base2 = String.sub eb 2 11 in
         let mant_base16 = String.sub sb 2 13 in
         let exp = int_of_string ("0b" ^ exp_base2) in
         if exp = 0 then (* subnormals *)
           let s = (if is_neg then "-" else "")^
                   "0x0."^mant_base16^"p-1023"
            in Float_hexa(s,float_of_string s)
           else if exp = 2047 then (* infinities and NaN *)
             if mant_base16="0000000000000" then
                if is_neg then Minus_infinity else Plus_infinity
                else Not_a_number
           else
           let exp = exp - 1023 in
           let s = (if is_neg then "-" else "")^
                   "0x1."^mant_base16^"p"^(string_of_int exp)
           in Float_hexa(s,float_of_string s)
      else
      if String.length eb = 4 && String.sub eb 0 2 = "#x" &&
         String.length sb = 25 && String.sub sb 0 2 = "#b" then
         (* binary 32 *)
         let exp_base16 = String.sub eb 2 2 in
         let mant_base2 = String.sub sb 2 23 in
         let mant_base16 =
           Format.asprintf "%06x" (2*int_of_string ("0b" ^ mant_base2))
         in
         let exp = int_of_string ("0x" ^ exp_base16) in
         if exp = 0 then (* subnormals *)
           let s = (if is_neg then "-" else "")^
                   "0x0."^mant_base16^"p-127"
            in Float_hexa(s,float_of_string s)
           else if exp = 255 then (* infinities and NaN *)
             if mant_base16="0000000" then
                if is_neg then Minus_infinity else Plus_infinity
                else Not_a_number
           else
           let exp = exp - 127 in
           let s = (if is_neg then "-" else "")^
                   "0x1."^mant_base16^"p"^(string_of_int exp)
           in Float_hexa(s,float_of_string s)
      else raise Exit
   with Exit -> Float_value (b, eb, sb)

95 96
type model_value =
 | Integer of string
97
 | Decimal of (string * string)
98
 | Fraction of (string * string)
99
 | Float of float_type
100
 | Boolean of bool
101
 | Array of model_array
102
 | Record of model_record
103
 | Proj of model_proj
104
 | Bitvector of string
105
 | Apply of string * model_value list
106
 | Unparsed of string
107
and  arr_index = {
108
  arr_index_key : string; (* Even array indices can exceed MAX_INT with Z3 *)
109 110 111 112 113 114
  arr_index_value : model_value;
}
and model_array = {
  arr_others  : model_value;
  arr_indices : arr_index list;
}
115

116
and model_record = (field_name * model_value) list
117 118
and model_proj = (proj_name * model_value)
and proj_name = string
119
and field_name = string
120 121 122 123 124 125 126 127

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

let array_add_element ~array ~index ~value =
128 129
  (*
     Adds the element value to the array on specified index.
130 131
  *)
  let arr_index = {
132
    arr_index_key = index;
133 134 135 136 137 138 139
    arr_index_value = value
  } in
  {
    arr_others = array.arr_others;
    arr_indices = arr_index::array.arr_indices;
  }

140 141 142
let convert_float_value f =
  match f with
  | Plus_infinity ->
143
      let m = Mstr.add "cons" (Json_base.String "Plus_infinity") Mstr.empty in
MARCHE Claude's avatar
MARCHE Claude committed
144
      Json_base.Record m
145
  | Minus_infinity ->
146
      let m = Mstr.add "cons" (Json_base.String "Minus_infinity") Mstr.empty in
MARCHE Claude's avatar
MARCHE Claude committed
147
      Json_base.Record m
148
  | Plus_zero ->
149
      let m = Mstr.add "cons" (Json_base.String "Plus_zero") Mstr.empty in
MARCHE Claude's avatar
MARCHE Claude committed
150
      Json_base.Record m
151
  | Minus_zero ->
152
      let m = Mstr.add "cons" (Json_base.String "Minus_zero") Mstr.empty in
MARCHE Claude's avatar
MARCHE Claude committed
153
      Json_base.Record m
154
  | Not_a_number ->
155
      let m = Mstr.add "cons" (Json_base.String "Not_a_number") Mstr.empty in
MARCHE Claude's avatar
MARCHE Claude committed
156
      Json_base.Record m
157
  | Float_value (b, eb, sb) ->
158
      let m = Mstr.add "cons" (Json_base.String "Float_value") Mstr.empty in
MARCHE Claude's avatar
MARCHE Claude committed
159 160 161 162
      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
163
  | Float_hexa(s,f) ->
164
      let m = Mstr.add "cons" (Json_base.String "Float_hexa") Mstr.empty in
165 166
      let m = Mstr.add "str_hexa" (Json_base.String s) m in
      let m = Mstr.add "value" (Json_base.Float f) m in
167
      Json_base.Record m
168

169
let rec convert_model_value value : Json_base.json =
170
  match value with
171
  | Integer s ->
172
      let m = Mstr.add "type" (Json_base.String "Integer") Mstr.empty in
173 174
      let m = Mstr.add "val" (Json_base.String s) m in
      Json_base.Record m
175
  | Float f ->
176
      let m = Mstr.add "type" (Json_base.String "Float") Mstr.empty in
177
      let m = Mstr.add "val" (convert_float_value f) m in
MARCHE Claude's avatar
MARCHE Claude committed
178
      Json_base.Record m
179
  | Decimal (int_part, fract_part) ->
180
      let m = Mstr.add "type" (Json_base.String "Decimal") Mstr.empty in
181 182
      let m = Mstr.add "val" (Json_base.String (int_part^"."^fract_part)) m in
      Json_base.Record m
183
  | Fraction (num, den) ->
184
      let m = Mstr.add "type" (Json_base.String "Fraction") Mstr.empty in
185 186
      let m = Mstr.add "val" (Json_base.String (num^"/"^den)) m in
      Json_base.Record m
187
  | Unparsed s ->
188
      let m = Mstr.add "type" (Json_base.String "Unparsed") Mstr.empty in
189 190
      let m = Mstr.add "val" (Json_base.String s) m in
      Json_base.Record m
191
  | Bitvector v ->
192
      let m = Mstr.add "type" (Json_base.String "Bv") Mstr.empty in
193 194
      let m = Mstr.add "val" (Json_base.String v) m in
      Json_base.Record m
195
  | Boolean b ->
196
      let m = Mstr.add "type" (Json_base.String "Boolean") Mstr.empty in
197 198
      let m = Mstr.add "val" (Json_base.Bool b) m in
      Json_base.Record m
199
  | Array a ->
200
      let l = convert_array a in
201
      let m = Mstr.add "type" (Json_base.String "Array") Mstr.empty in
202 203
      let m = Mstr.add "val" (Json_base.List l) m in
      Json_base.Record m
204 205 206
  | Apply (s, lt) ->
      let lt = List.map convert_model_value lt in
      let slt =
207
        let m = Mstr.add "list" (Json_base.List lt) Mstr.empty in
208 209 210
        let m = Mstr.add "apply" (Json_base.String s) m in
        Json_base.Record m
      in
211
      let m = Mstr.add "type" (Json_base.String "Apply") Mstr.empty in
212 213
      let m = Mstr.add "val" slt m in
      Json_base.Record m
214 215
  | Record r ->
      convert_record r
216 217
  | Proj p ->
      convert_proj p
218 219 220

and convert_array a =
  let m_others =
221
    Mstr.add "others" (convert_model_value a.arr_others) Mstr.empty in
222
  convert_indices a.arr_indices @ [Json_base.Record m_others]
223 224 225 226 227

and convert_indices indices =
  match indices with
  | [] -> []
  | index :: tail ->
228
    let m = Mstr.add "indice" (Json_base.String index.arr_index_key) Mstr.empty in
229
    let m = Mstr.add "value" (convert_model_value index.arr_index_value) m in
230
    Json_base.Record m :: convert_indices tail
231 232

and convert_record r =
233
  let m = Mstr.add "type" (Json_base.String "Record") Mstr.empty in
234
  let fields = convert_fields r in
235
  let m_field = Mstr.add "Field" fields Mstr.empty in
236
  let m = Mstr.add "val" (Json_base.Record m_field) m in
237
  Json_base.Record m
238

239 240 241 242 243 244 245
and convert_proj p =
  let proj_name, value = p in
  let m = Mstr.add "type" (Json_base.String "Proj") Mstr.empty in
  let m = Mstr.add "proj_name" (Json_base.String proj_name) m in
  let m = Mstr.add "value" (convert_model_value value) m in
  Json_base.Proj m

246
and convert_fields fields =
247 248 249
  Json_base.List
    (List.map
       (fun (f, v) ->
250
         let m = Mstr.add "field" (Json_base.String f) Mstr.empty in
251 252 253
         let m = Mstr.add "value" (convert_model_value v) m in
         Json_base.Record m)
       fields)
254 255 256

let print_model_value_sanit fmt v =
  let v = convert_model_value v in
257
  Json_base.print_json fmt v
258

259
let print_model_value = print_model_value_sanit
260

261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277

(******************************************)
(* 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) ->
278
     fprintf fmt "float_bits(%s,%s,%s)" b eb sb
279
  | Float_hexa(s,f) -> fprintf fmt "%s (%g)" s f
280 281

let rec print_array_human fmt (arr: model_array) =
282
  fprintf fmt "@[(";
283
  List.iter (fun e ->
284
    fprintf fmt "@[%s =>@ %a,@]" e.arr_index_key print_model_value_human e.arr_index_value)
285
    arr.arr_indices;
286
  fprintf fmt "@[others =>@ %a@])@]" print_model_value_human arr.arr_others
287 288

and print_record_human fmt r =
289
  fprintf fmt "@[%a@]"
290
    (Pp.print_list_delim ~start:Pp.lbrace ~stop:Pp.rbrace ~sep:Pp.semi
291
    (fun fmt (f, v) -> fprintf fmt "@[%s =@ %a@]" f print_model_value_human v)) r
292

293 294
and print_proj_human fmt p =
  let s, v = p in
295
  fprintf fmt "@[{%s =>@ %a}@]"
296 297
    s print_model_value_human v

298 299 300 301
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)
302
  | Fraction (s1, s2) -> fprintf fmt "%s" (s1 ^ "/" ^ s2)
303 304
  | Float f -> print_float_human fmt f
  | Boolean b -> fprintf fmt "%b"  b
305 306
  | Apply (s, []) ->
      fprintf fmt "%s" s
307
  | Apply (s, lt) ->
308
    fprintf fmt "@[(%s@ %a)@]" s (Pp.print_list Pp.space print_model_value_human) lt
309 310
  | Array arr -> print_array_human fmt arr
  | Record r -> print_record_human fmt r
311
  | Proj p -> print_proj_human fmt p
312 313 314
  | Bitvector s -> fprintf fmt "%s" s
  | Unparsed s -> fprintf fmt "%s" s

315
(*
316
***************************************************************
317 318 319
**  Model elements
***************************************************************
*)
320 321

type model_element_kind =
322 323
| Result
| Old
324
| Error_message
325 326
| Other

327 328 329
type model_element_name = {
  men_name   : string;
  men_kind   : model_element_kind;
Guillaume Melquiond's avatar
Guillaume Melquiond committed
330 331
  (* Attributes associated to the id of the men *)
  men_attrs : Sattr.t;
332 333
}

334
type model_element = {
335
  me_name     : model_element_name;
336
  me_value    : model_value;
337 338
  me_location : Loc.position option;
  me_term     : Term.term option;
339
}
340

341
let split_model_trace_name mt_name =
342 343
  (* Mt_name is of the form "name[@type[@*]]". Return (name, type) *)
  let splitted = Strings.bounded_split '@' mt_name 3 in
344 345
  match splitted with
  | [first] -> (first, "")
346 347
  | first::second::_ -> (first, second)
  | [] -> ("", "")
348

349
let create_model_element ~name ~value ?location ?term () =
350
  let (name, type_s) = split_model_trace_name name in
351
  let me_kind = match type_s with
352 353 354
    | "result" -> Result
    | "old" -> Old
    | _ -> Other in
355 356 357
  let me_name = {
    men_name = name;
    men_kind = me_kind;
Guillaume Melquiond's avatar
Guillaume Melquiond committed
358
    men_attrs = match term with | None -> Sattr.empty | Some t -> t.t_attrs;
359
  } in
360
  {
361
    me_name = me_name;
362 363
    me_value = value;
    me_location = location;
364
    me_term = term;
365 366
  }

Guillaume Melquiond's avatar
Guillaume Melquiond committed
367
let construct_name (name: string) attrs : model_element_name =
368 369 370 371 372
  let (name, type_s) = split_model_trace_name name in
  let me_kind = match type_s with
  | "result" -> Result
  | "old" -> Old
  | _ -> Other in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
373
  {men_name = name; men_kind = me_kind; men_attrs = attrs}
374

375
(*
376 377 378 379
let print_location fmt m_element =
    match m_element.me_location with
    | None -> fprintf fmt "\"no location\""
    | Some loc -> Loc.report_position fmt loc
380
*)
381 382

(*
383
***************************************************************
384 385
**  Model definitions
***************************************************************
386
*)
387 388
module IntMap = Mint
module StringMap = Mstr
389 390

type model_file = model_element list IntMap.t
391 392 393 394 395
type model_files = model_file StringMap.t
type model = {
  vc_term_loc : Loc.position option;
  model_files : model_files;
}
396 397 398

let empty_model = StringMap.empty
let empty_model_file = IntMap.empty
399 400 401 402 403 404
let is_model_empty model =
  model.model_files = empty_model
let default_model = {
  vc_term_loc = None;
  model_files = empty_model;
}
405 406 407

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

408
type raw_model_parser =
409
  Sstr.t -> ((string * string) list) Mstr.t -> string list ->
410
    string -> model_element list
411 412

(*
413
***************************************************************
414 415 416
**  Quering the model
***************************************************************
*)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
417
let print_model_element ~print_attrs print_model_value me_name_trans fmt m_element =
418 419
  match m_element.me_name.men_kind with
  | Error_message ->
420
    fprintf fmt "%s" m_element.me_name.men_name
421
  | _ ->
422
    let me_name = me_name_trans m_element.me_name in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
423
    if print_attrs then
424 425
      fprintf fmt  "%s, [%a] = %a"
        me_name
Guillaume Melquiond's avatar
Guillaume Melquiond committed
426 427
        (Pp.print_list Pp.comma Pretty.print_attr)
        (Sattr.elements m_element.me_name.men_attrs)
428 429 430 431 432 433
        print_model_value m_element.me_value
    else
      fprintf fmt  "%s = %a"
        me_name
        print_model_value m_element.me_value

Guillaume Melquiond's avatar
Guillaume Melquiond committed
434 435
let print_model_elements ~print_attrs ?(sep = "\n") print_model_value me_name_trans fmt m_elements =
  Pp.print_list (fun fmt () -> Pp.string fmt sep) (print_model_element ~print_attrs print_model_value me_name_trans) fmt m_elements
436

Guillaume Melquiond's avatar
Guillaume Melquiond committed
437
let print_model_file ~print_attrs ~print_model_value fmt me_name_trans filename model_file =
MARCHE Claude's avatar
MARCHE Claude committed
438
  (* Relativize does not work on nighly bench: using basename instead. It
439
     hides the local paths.  *)
MARCHE Claude's avatar
MARCHE Claude committed
440
  let filename = Filename.basename filename  in
441
  fprintf fmt "File %s:" filename;
442
  IntMap.iter
443
    (fun line m_elements ->
444
      fprintf fmt "@\nLine %d:@\n" line;
Guillaume Melquiond's avatar
Guillaume Melquiond committed
445
      print_model_elements ~print_attrs print_model_value me_name_trans fmt m_elements)
446 447
    model_file;
  fprintf fmt "@\n"
448

449 450
let why_name_trans me_name =
  match me_name.men_kind with
451
  | Result -> "result"
452
  | Old    -> "old" ^ " " ^ me_name.men_name
453
  | _  -> me_name.men_name
454 455

let print_model
Guillaume Melquiond's avatar
Guillaume Melquiond committed
456
    ~print_attrs
457
    ?(me_name_trans = why_name_trans)
458
    ~print_model_value
459
    fmt
460
    model =
461 462 463
  StringMap.iter (fun k e ->
      print_model_file ~print_attrs ~print_model_value fmt me_name_trans k e)
    model.model_files
464 465 466 467

let print_model_human
    ?(me_name_trans = why_name_trans)
    fmt
468 469
    model =
  print_model ~me_name_trans ~print_model_value:print_model_value_human fmt model
470 471

let print_model ?(me_name_trans = why_name_trans)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
472
    ~print_attrs
473
    fmt
Guillaume Melquiond's avatar
Guillaume Melquiond committed
474
    model = print_model ~print_attrs ~me_name_trans ~print_model_value fmt model
475

476
let model_to_string
Guillaume Melquiond's avatar
Guillaume Melquiond committed
477
    ~print_attrs
478 479
    ?(me_name_trans = why_name_trans)
    model =
Guillaume Melquiond's avatar
Guillaume Melquiond committed
480
  Format.asprintf "%a" (print_model ~print_attrs ~me_name_trans) model
481

482 483 484 485 486
let get_model_file model filename =
  try
    StringMap.find filename model
  with Not_found ->
    empty_model_file
487

488 489 490 491 492
let get_elements model_file line_number =
  try
    IntMap.find line_number model_file
  with Not_found ->
    []
493

494
(* TODO unused
495
let print_model_vc_term
Guillaume Melquiond's avatar
Guillaume Melquiond committed
496
    ~print_attrs
497 498 499 500
    ?(me_name_trans = why_name_trans)
    ?(sep = "\n")
    fmt
    model =
501 502 503 504 505 506 507
  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
Guillaume Melquiond's avatar
Guillaume Melquiond committed
508
      print_model_elements ~print_attrs ~sep print_model_value me_name_trans fmt model_elements
509

510
let model_vc_term_to_string
Guillaume Melquiond's avatar
Guillaume Melquiond committed
511
    ~print_attrs
512 513 514
    ?(me_name_trans = why_name_trans)
    ?(sep = "\n")
    model =
Guillaume Melquiond's avatar
Guillaume Melquiond committed
515
  Format.asprintf "%a" (print_model_vc_term ~print_attrs ~me_name_trans ~sep) model
516
*)
517

518
let get_padding line =
519
  try
520 521 522 523 524
    let r = Str.regexp " *" in
    ignore (Str.search_forward r line 0);
    Str.matched_string line
  with Not_found -> ""

525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550
(* 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)

551
let interleave_line
Guillaume Melquiond's avatar
Guillaume Melquiond committed
552
    ~print_attrs
553 554 555 556
    start_comment
    end_comment
    me_name_trans
    model_file
557
    (source_code, line_number, offset, remaining_locs, locs)
558
    line =
559 560 561 562
  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
563 564
  try
    let model_elements = IntMap.find line_number model_file in
565
    let cntexmp_line =
566 567 568
      asprintf "%s%s%a%s"
        (get_padding line)
        start_comment
Guillaume Melquiond's avatar
Guillaume Melquiond committed
569
        (print_model_elements ~print_attrs ~sep:"; " print_model_value_human me_name_trans) model_elements
570
        end_comment in
571

572 573 574 575 576 577 578
    (* 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)
579
  with Not_found ->
580
    (source_code ^ line, line_number + 1, offset, remaining_locs, list_loc @ locs)
581

582 583

let interleave_with_source
Guillaume Melquiond's avatar
Guillaume Melquiond committed
584
    ~print_attrs
585 586
    ?(start_comment="(* ")
    ?(end_comment=" *)")
587
    ?(me_name_trans = why_name_trans)
588
    model
589 590 591 592 593 594 595
    ~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
596
  try
597 598 599 600 601 602 603 604 605
    (* 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
606 607
    let src_lines_up_to_last_cntexmp_el source_code model_file =
      let (last_cntexmp_line, _) = IntMap.max_binding model_file in
608 609
      Str.bounded_split (Str.regexp "^") source_code (last_cntexmp_line+1)
    in
610 611
    let (source_code, _, _, _, gen_loc) =
      List.fold_left
Guillaume Melquiond's avatar
Guillaume Melquiond committed
612
        (interleave_line ~print_attrs
613 614 615 616 617
           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
618
  with Not_found ->
619
    source_code, locations
620

Guillaume Melquiond's avatar
Guillaume Melquiond committed
621 622 623
let print_attrs_json (me: model_element_name) fmt =
  Json_base.list (fun fmt attr -> Json_base.string fmt attr.attr_string) fmt
    (Sattr.elements me.men_attrs)
624 625 626 627

(*
**  Quering the model - json
*)
628 629
let print_model_element_json me_name_to_str fmt me =
  let print_value fmt =
630
    fprintf fmt "%a" print_model_value_sanit me.me_value in
631 632
  let print_kind fmt =
    match me.me_name.men_kind with
633 634 635 636
    | 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
637
  let print_name fmt =
638
    Json_base.string fmt (me_name_to_str me) in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
639 640
  let print_json_attrs fmt =
    print_attrs_json me.me_name fmt in
641 642
  let print_value_or_kind_or_name fmt printer =
    printer fmt in
643
  Json_base.map_bindings
644 645 646 647
    (fun s -> s)
    print_value_or_kind_or_name
    fmt
    [("name", print_name);
Guillaume Melquiond's avatar
Guillaume Melquiond committed
648
     ("attrs", print_json_attrs);
649 650
     ("value", print_value);
     ("kind", print_kind)]
651

652
let print_model_elements_json me_name_to_str fmt model_elements =
653
  Json_base.list
654
    (print_model_element_json me_name_to_str)
655
    fmt
656
    model_elements
657

658 659
let print_model_elements_on_lines_json model me_name_to_str vc_line_trans fmt
    (file_name, model_file) =
660
  Json_base.map_bindings
661 662 663 664 665 666 667 668 669 670 671
    (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
    )
672
    (print_model_elements_json me_name_to_str)
673 674
    fmt
    (IntMap.bindings model_file)
675

676 677
let print_model_json
    ?(me_name_trans = why_name_trans)
678
    ?(vc_line_trans = (fun i -> string_of_int i))
679
    fmt
680
    model =
681
  let me_name_to_str = fun me ->
682
    me_name_trans me.me_name in
683 684 685 686 687
  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
688
  Json_base.map_bindings
689
    (fun s -> s)
690
    (print_model_elements_on_lines_json model me_name_to_str vc_line_trans)
691
    fmt
692
    model_files_bindings
693

694 695
let model_to_string_json
    ?(me_name_trans = why_name_trans)
696
    ?(vc_line_trans = (fun i -> string_of_int i))
697
    model =
698
  asprintf "%a" (print_model_json ~me_name_trans ~vc_line_trans) model
699

700

701
(*
702
***************************************************************
703 704 705 706 707 708 709 710 711 712 713 714 715 716 717
**  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

718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765
let recover_name term_map raw_name =
  let t = Mstr.find raw_name term_map in
  construct_name (get_model_trace_string ~attrs:t.t_attrs) t.t_attrs

let rec replace_projection (const_function: string -> string) model_value =
  match model_value with
  | Integer _ | Decimal _ | Fraction _ | Float _ | Boolean _ | Bitvector _
    | Unparsed _ -> model_value
  | Array a ->
      Array (replace_projection_array const_function a)
  | Record r ->
      let r =
        List.map (fun (field_name, value) ->
          let field_name = try const_function field_name with
            Not_found -> field_name
          in
          (field_name, replace_projection const_function value)
          )
          r
      in
      Record r
  | Proj p ->
      let proj_name, value = p in
      let proj_name =
        try const_function proj_name
        with Not_found -> proj_name
      in
      Proj (proj_name, replace_projection const_function value)
  | Apply (s, l) ->
      let s = try const_function s
        with Not_found -> s
      in
      Apply (s, (List.map (fun v -> replace_projection const_function v) l))

and replace_projection_array const_function a =
  let {arr_others = others; arr_indices = arr_index_list} = a in
  let others = replace_projection const_function others in
  let arr_index_list =
    List.map
      (fun ind ->
         let {arr_index_key = key; arr_index_value = value} = ind in
         let value = replace_projection const_function value in
         {arr_index_key = key; arr_index_value = value}
      )
      arr_index_list
  in
  {arr_others = others; arr_indices = arr_index_list}

766 767 768
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
769
    let raw_element_value = replace_projection (fun x -> (recover_name term_map x).men_name) raw_element.me_value in
770 771 772 773
    try
      (
       let t = Mstr.find raw_element_name term_map in
       let model_element = {
774 775 776 777
         me_name = construct_name (get_model_trace_string ~attrs:t.t_attrs) t.t_attrs;
         me_value = raw_element_value;
         me_location = t.t_loc;
         me_term = Some t;
778 779 780 781 782 783
       } in
       add_to_model model model_element
      )
    with Not_found -> model)
    model
    raw_model
784

785 786
let handle_contradictory_vc model_files vc_term_loc =
  (* The VC is contradictory if the location of the term that triggers VC
787 788
     was collected, model_files is not empty, and there are no model elements
     in this location.
789 790
     If this is the case, add model element saying that VC is contradictory
     to this location. *)
791 792 793 794 795 796 797 798 799 800 801 802 803
  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  *)
804 805
	let me_name = {
	  men_name = "the check fails with all inputs";
806
	  men_kind = Error_message;
Guillaume Melquiond's avatar
Guillaume Melquiond committed
807
          men_attrs = Sattr.empty;
808
	} in
809
	let me = {
810
	  me_name = me_name;
811 812 813 814 815 816 817
	  me_value = Unparsed "";
	  me_location = Some pos;
	  me_term = None;
	} in
	add_to_model model_files me
      else
	model_files
818

819
let build_model raw_model printer_mapping =
820
  let model_files = build_model_rec raw_model printer_mapping.queried_terms empty_model in
821
  let model_files = handle_contradictory_vc model_files printer_mapping.Printer.vc_term_loc in
822 823