collect_data_model.ml 12.6 KB
Newer Older
1 2 3 4 5 6 7
open Stdlib
open Smt2_model_defs
open Strings

exception Not_value

(* Adds all referenced cvc4 variables found in the term t to table *)
Sylvain Dailler's avatar
Sylvain Dailler committed
8
let rec get_variables_term (table: correspondence_table) t =
9 10
  match t with
  | Variable _ | Function_Local_Variable _ | Boolean _ | Integer _
11
  | Decimal _ | Float _ | Other _ | Bitvector _ -> table
12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41
  | Array a ->
    get_variables_array table a
  | Ite (t1, t2, t3, t4) ->
    let table = get_variables_term table t1 in
    let table = get_variables_term table t2 in
    let table = get_variables_term table t3 in
    let table = get_variables_term table t4 in
    table
  | Cvc4_Variable cvc ->
    if Mstr.mem cvc table then
      table
    else
      Mstr.add cvc (false, Noelement) table
  | Record (_, l) ->
    List.fold_left (fun table t -> get_variables_term table t) table l
  | Discr (_, l) ->
    List.fold_left (fun table t -> get_variables_term table t) table l
  | To_array t ->
    get_variables_term table t

and get_variables_array table a =
   match a with
   | Const t ->
    let table = get_variables_term table t in
    table
   | Store (a, t1, t2) ->
     let table = get_variables_array table a in
     let table = get_variables_term table t1 in
     get_variables_term table t2

Sylvain Dailler's avatar
Sylvain Dailler committed
42
let get_all_var (table: correspondence_table) =
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 79 80 81 82 83 84 85 86 87 88 89 90
  Mstr.fold (fun _key element table ->
    match element with
    | _, Noelement -> table
    | _, Function (_, t) -> get_variables_term table t
    | _, Term t -> get_variables_term table t) table table

(* Return true if key is s suffixed with a number *)
(* We should change the code of this function (Str still forbidden) *)
let is_prefix_num key s =
  if (String.length s >= String.length key) || String.length s = 0 then
    false
  else
    try
      let b = ref (has_prefix s key) in
      for i = String.length s to String.length key - 1 do
        b := !b && (String.get key i <= '9') && (String.get key i >= '0')
      done;
      !b
    with
    | _ -> false

(* Add all variables referenced in the model to the table *)
let add_all_cvc s table t =
  Mstr.fold (fun key _element acc ->
    if is_prefix_num key s then
      try
        if snd (Mstr.find key acc) = Noelement then
          Mstr.add key t acc
        else acc
      with Not_found -> acc
    else
      acc) table table

exception Bad_variable

(* Get the "radical" of a variable *)
let remove_end_num s =
  let n = ref (String.length s - 1) in
  while String.get s !n <= '9' && String.get s !n >= '0' && !n >= 0 do
    n := !n - 1
  done;
  try
    String.sub s 0 (!n + 1)
  with
  | _ -> s

(* Add the variables that can be deduced from ITE to the table of variables *)
let add_vars_to_table table value =
Sylvain Dailler's avatar
Sylvain Dailler committed
91
  let rec add_vars_to_table (table: correspondence_table) value =
92 93 94 95 96 97 98 99 100 101 102 103 104 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
    let t = match (snd value) with
    | Term t -> t
    | Function (_, t) -> t
    | Noelement -> raise Bad_variable in
    match t with
    | Ite (Cvc4_Variable cvc, Function_Local_Variable _x, t1, t2) ->
        begin
          let table = Mstr.add cvc (false, Term t1) table in
          add_vars_to_table table (false, Term t2)
        end
    | Ite (Function_Local_Variable _x, Cvc4_Variable cvc, t1, t2) ->
        begin
          let table = Mstr.add cvc (false, Term t1) table in
          add_vars_to_table table (false, Term t2)
        end
    | Ite (t, Function_Local_Variable _x, Cvc4_Variable cvc, t2) ->
        begin
          let table = Mstr.add cvc (false, Term t) table in
          add_vars_to_table table (false, Term t2)
        end
    | Ite (Function_Local_Variable _x, t, Cvc4_Variable cvc, t2) ->
        begin
          let table = Mstr.add cvc (false, Term t) table in
          add_vars_to_table table (false, Term t2)
        end
    | Ite (_, _, _, _) -> table
    | _ -> table
  in
  add_vars_to_table table value

let rec refine_definition table t =
  match t with
  | Term t -> Term (refine_function table t)
  | Function (vars, t) -> Function (vars, refine_function table t)
  | Noelement -> Noelement

and refine_array table a =
  match a with
  | Const t ->
    let t = refine_function table t in
    Const t
  | Store (a, t1, t2) ->
    let a = refine_array table a in
    let t1 = refine_function table t1 in
    let t2 = refine_function table t2 in
    Store (a, t1, t2)

(* This function takes the table of assigned variables and a term and replace
   the variables with the constant associated with them in the table. If their
   value is not a constant yet, recursively apply on these variables and update
   their value. *)
and refine_function table term =
  match term with
145
  | Integer _ | Decimal _ | Float _ | Other _ | Bitvector _ | Boolean _ -> term
146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 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
  | Cvc4_Variable v ->
    begin
      try (
      let (b, t) = Mstr.find v table in
      let t = match t with
      | Term t -> t
      | Function (_vars, t) -> t
      | Noelement -> raise Not_value
      in
      if b then
        t
      else
        let table = refine_variable_value table v (b, Term t) in
        let t = match (snd (Mstr.find v table)) with
        | Term t -> t
        | Function (_vars, t) -> t
        | Noelement -> raise Not_value in
        t
       ) with
      | Not_found -> term
      | Not_value -> term
    end
  | Function_Local_Variable _ -> term
  | Variable _ -> term
  | Ite (t1, t2, t3, t4) ->
    let t1 = refine_function table t1 in
    let t2 = refine_function table t2 in
    let t3 = refine_function table t3 in
    let t4 = refine_function table t4 in
    Ite (t1, t2, t3, t4)
  | Array a ->
    Array (refine_array table a)
  | Record (n, l) ->
    Record (n, List.map (fun x -> refine_function table x) l)
  | Discr (n, l) ->
    Discr (n, List.map (fun x -> refine_function table x) l)
  | To_array t ->
    To_array (refine_function table t)


Sylvain Dailler's avatar
Sylvain Dailler committed
186
and refine_variable_value (table: correspondence_table) key v =
187 188 189 190 191 192 193
  let (b, t) = v in
  if b then
    table
  else
    let tv = refine_definition table t in
    Mstr.add key (true, tv) table

194 195 196 197 198 199 200 201
let convert_float (f: Smt2_model_defs.float_type) : Model_parser.float_type =
  match f with
  | Plus_infinity           -> Model_parser.Plus_infinity
  | Minus_infinity          -> Model_parser.Minus_infinity
  | Plus_zero               -> Model_parser.Plus_zero
  | Minus_zero              -> Model_parser.Minus_zero
  | Not_a_number            -> Model_parser.Not_a_number
  | Float_value (b, eb, sb) -> Model_parser.Float_value (b, eb, sb)
202 203 204 205 206 207

(* Conversion to value referenced as defined in model_parser.
   We assume that array indices fit into an integer *)
let convert_to_indice t =
  match t with
  | Integer i -> i
208
  | Bitvector bv -> bv
209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229
  | _ -> raise Not_value

let rec convert_array_value (a: array) : Model_parser.model_array =
  let array_indices = ref [] in

  let rec create_array_value a =
    match a with
    | Const t -> { Model_parser.arr_indices = !array_indices;
                   Model_parser.arr_others = convert_to_model_value t}
    | Store (a, t1, t2) ->
        let new_index =
          { Model_parser.arr_index_key = convert_to_indice t1;
            Model_parser.arr_index_value = convert_to_model_value t2} in
        array_indices := new_index :: !array_indices;
        create_array_value a in
  create_array_value a

and convert_to_model_value (t: term): Model_parser.model_value =
  match t with
  | Integer i -> Model_parser.Integer i
  | Decimal (d1, d2) -> Model_parser.Decimal (d1, d2)
230
  | Float f -> Model_parser.Float (convert_float f)
231 232 233 234 235 236 237 238 239
  | Bitvector bv -> Model_parser.Bitvector bv
  | Boolean b -> Model_parser.Boolean b
  | Other _s -> raise Not_value
  | Array a -> Model_parser.Array (convert_array_value a)
  | Record (_n, l) ->
      Model_parser.Record (convert_record l)
  | Cvc4_Variable _v -> Model_parser.Unparsed "!"
  (* TODO change the value returned for non populated Cvc4 variable '!' -> '?' ? *)
  | To_array t -> convert_to_model_value (Array (convert_z3_array t))
240
  | Function_Local_Variable _ | Variable _ | Ite _ | Discr _ -> raise Not_value
241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330

and convert_z3_array (t: term) : array =

  let rec convert_array t =
    match t with
    (* This works for multidim array because, we call convert_to_model_value on
       the new array generated (which will still contain a To_array).
       Example of value for multidim array:
       To_array (Ite (x, 1, (To_array t), To_array t')) -> call on complete term ->
       Store (1, To_array t, To_array t') -> call on subpart (To_array t) ->
       Store (1, Const t, To_array t') -> call on subpart (To_array t') ->
       Store (1, Const t, Const t')
     *)

    | Ite (Function_Local_Variable _x, if_t, t1, t2) ->
      Store (convert_array t2, if_t, t1)
    | Ite (if_t, Function_Local_Variable _x, t1, t2) ->
      Store (convert_array t2, if_t, t1)
    | t -> Const t
  in
  convert_array t

and convert_record l =
  let acc = ref [] in
  let rec convert_aux l =
    match l with
    | Discr (_n, l) :: tl ->
        acc := List.map convert_to_model_value l;
        convert_aux tl
    | a :: tl ->
        convert_to_model_value a :: convert_aux tl
    | [] -> []
  in
  let record_field = convert_aux l in
  {
    Model_parser.discrs = !acc;
    Model_parser.fields = record_field
  }

let convert_to_model_element name t =
  match t with
  | None -> raise Not_value
  | Some t ->
      let value = convert_to_model_value t in
      Model_parser.create_model_element ~name ~value ()

(* Printing function *)
let print_table t =
  Format.eprintf "Table key and value@.";
  Mstr.iter (fun key e -> Format.eprintf "%s %a@." key print_def (snd e)) t;
  Format.eprintf "End table@."


(* Analysis function to get the value of Cvc4 variable contained in the model *)

(* Given a to_rep and its corresponding of_rep in the model gives a guessed
   value to unknown variables using constant of_rep/to_rep and "else" case of
   the ITE.*)
let corres_else_element table to_rep of_rep =
  let (_key1, (_b1, to_rep)) = to_rep in
  let (_key2, (_b2, of_rep)) = of_rep in
  let to_rep = match to_rep with
  | Term t -> t
  | Function (_, t) -> t
  | Noelement -> raise Not_value in

  let of_rep = match of_rep with
  | Term t -> t
  | Function (_, t) -> t
  | Noelement -> raise Not_value in

  let rec corres_else_element table to_rep of_rep =
    match (to_rep, of_rep) with
    | Ite (_, _, _, to_rep), _ -> corres_else_element table to_rep of_rep
    | _, Ite (_, _, _, of_rep) -> corres_else_element table to_rep of_rep
    | t, Cvc4_Variable cvc ->
        (* Make all variables not already guessed equal to the else case *)
        let s = remove_end_num cvc in
        add_all_cvc s table (false, Term t)
    | _ -> table
  in
  (* Case where to_rep, of_rep are constant values *)
  let table =
    match (to_rep, of_rep) with
    | t, Cvc4_Variable cvc ->
        Mstr.add cvc (false, Term t) table
    | _ -> table
  in
  corres_else_element table to_rep of_rep

Sylvain Dailler's avatar
Sylvain Dailler committed
331
let to_rep_of_rep (table: correspondence_table) =
332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353
  let to_reps =
    List.sort (fun x y -> String.compare (fst x) (fst y))
      (Mstr.fold (fun key value acc ->
        if has_prefix "to_rep" key then
        (key,value) :: acc else acc) table []) in

  let of_reps =
    List.sort (fun x y -> String.compare (fst x) (fst y))
      (Mstr.fold (fun key value acc -> if has_prefix "of_rep" key then
        (key,value) :: acc else acc) table []) in

  let rec to_rep_of_rep table to_reps of_reps =
    match to_reps, of_reps with
    | to_rep :: tl1, of_rep :: tl2 ->
      let table = corres_else_element table to_rep of_rep in
      to_rep_of_rep table tl1 tl2
    | [], [] -> table
    | _ -> table (* Error case *) in

  to_rep_of_rep table to_reps of_reps


Sylvain Dailler's avatar
Sylvain Dailler committed
354
let create_list (table: correspondence_table) =
355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379

  (* First populate the table with all references to a cvc variable *)
  let table = get_all_var table in

  (* First recover the values of variables that can be recovered in to/of_rep *)
  let table =
    Mstr.fold (fun key value acc ->
      if has_prefix "of_rep" key && not (String.contains key '!') then
        add_vars_to_table acc value else acc) table table in

  (* of_rep is done before to_rep because we complete from value with the
     else branch of the function *)
  let table =
    Mstr.fold (fun key value acc ->
      if has_prefix "to_rep" key && not (String.contains key '!') then
        add_vars_to_table acc value else acc) table table in

  (* Recover values from the combination of to_rep and of_rep *)
  let table = to_rep_of_rep table in

  (* Then substitute all variables with their values *)
  let table =
    Mstr.fold (fun key v acc -> refine_variable_value acc key v) table table in

  (* Then converts all variables to raw_model_element *)
380 381 382 383 384 385 386 387
  Mstr.fold
    (fun key value list_acc ->
      let t = match value with
      | (_, Term t) ->
          Some t
      | (_, Function ([], t)) ->
          Some t
      | _ -> None in
388
      try (convert_to_model_element key t :: list_acc)
389 390 391
      with Not_value -> list_acc)
    table
    []