model_parser.ml 7.37 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 18 19 20 21 22
open Term
open Ident
open Printer

(*
*************************************************************** 
**  Counter-example model values
****************************************************************
*)
23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 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

type model_value =
 | Integer of string
 | Array of model_array
 | Other of string
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 =
  (* 
     Adds the element value to the array on specified index. 
  *)
  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;
  }

let rec print_indices fmt indices =
  match indices with
  | [] -> ()
  | index::tail ->
    fprintf fmt "; %d -> " index.arr_index_key;
    print_model_value fmt index.arr_index_value;
    print_indices fmt tail
and
print_array fmt arr = 
  fprintf fmt "{others -> ";
  print_model_value fmt arr.arr_others;
  print_indices fmt arr.arr_indices;
  fprintf fmt "}"
and
print_model_value fmt value =
  (* Prints model value. *)
  match value with
  | Integer s -> fprintf fmt "%s" s  
  | Other s -> fprintf fmt "%s" s
  | Array a -> print_array fmt a
79

80 81 82 83 84 85

(*
*************************************************************** 
**  Model elements
***************************************************************
*)
86 87
type model_element = { 
  me_name     : string;
88
  me_value    : model_value;
89 90
  me_location : Loc.position option;
  me_term     : Term.term option;
91
}
92

93
let create_model_element ~name ~value ?location ?term () =
94 95 96 97
  {
    me_name = name;
    me_value = value;
    me_location = location;
98
    me_term = term;
99 100 101 102 103 104
  }

let print_location fmt m_element =
    match m_element.me_location with
    | None -> fprintf fmt "\"no location\""
    | Some loc -> Loc.report_position fmt loc
105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144


(*
*************************************************************** 
**  Model definitions
***************************************************************
*)   
module IntMap = Map.Make(struct type t  = int let compare = compare end)
module StringMap = Map.Make(String)

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

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

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

type raw_model_parser =  string -> model_element list

(*
*************************************************************** 
**  Quering the model
***************************************************************
*)

let print_model_element fmt m_element =
  fprintf fmt  "    %s = %a\n" 
      m_element.me_name print_model_value m_element.me_value

let print_model_elements fmt line m_elements =
  fprintf fmt "  Line %d:\n" line;
  List.iter (print_model_element fmt) m_elements

let print_model_file fmt filename model_file =
  fprintf fmt "File %s:\n" filename;
  IntMap.iter (print_model_elements fmt) model_file

let print_model fmt model =
  StringMap.iter (print_model_file fmt) model
145 146 147 148 149

let model_to_string model =
  print_model str_formatter model;
  flush_str_formatter ()

150 151 152 153 154
let get_model_file model filename =
  try
    StringMap.find filename model
  with Not_found ->
    empty_model_file
155

156 157 158 159 160
let get_elements model_file line_number =
  try
    IntMap.find line_number model_file
  with Not_found ->
    []
161

162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231
(*
*************************************************************** 
**  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
    begin 
      try 
	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
    
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 ->
    let (element_name, element_location, element_term, terms_tail) = 
      match terms with
      | [] -> (model_element.me_name, None, None, [])
      | term::t_tail -> 
        ((get_element_name term model_element.me_name), 
         term.t_loc, 
         Some term, t_tail) in
    let new_model_element = create_model_element
      ~name:element_name 
      ~value:model_element.me_value 
      ?location:element_location 
      ?term:element_term 
      () in
    let model = add_to_model model new_model_element in
    build_model_rec 
      raw_strings_tail 
      terms_tail 
      model
  

let build_model raw_model printer_mapping =
  build_model_rec raw_model printer_mapping.queried_terms empty_model


(*
*************************************************************** 
** Registering model parser
***************************************************************
*)
232 233 234 235

exception KnownModelParser of string
exception UnknownModelParser of string

236 237 238 239 240 241 242 243 244
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

245 246 247 248
let register_model_parser ~desc s p =
  if Hstr.mem model_parsers s then raise (KnownModelParser s);
  Hstr.replace model_parsers s (desc, p)

249
let lookup_raw_model_parser s =
250 251 252
  try snd (Hstr.find model_parsers s)
  with Not_found -> raise (UnknownModelParser s)

253 254 255
let lookup_model_parser s =
  make_mp_from_raw (lookup_raw_model_parser s)

256 257 258 259 260
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"
261
  (fun _ -> [])