Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

eval_match.ml 6.13 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11 12 13 14 15

open Ident
open Ty
open Term
open Decl
Andrei Paskevich's avatar
Andrei Paskevich committed
16
open Pdecl
17

Andrei Paskevich's avatar
Andrei Paskevich committed
18 19 20
let is_projection kn ls = ls.ls_constr = 0 &&
  match Mid.find ls.ls_name kn with
  | { pd_node = PDtype _ } -> true
21 22
  | _ -> false

Andrei Paskevich's avatar
Andrei Paskevich committed
23 24 25 26 27 28 29 30 31 32 33 34 35
let find_constructors kn ({ts_name = id} as ts) =
  let rec find = function
    | {d_news = s}::dl when not (Mid.mem id s) -> find dl
    | {d_node = Ddata dl}::_ -> List.assq ts dl
    | _ -> [] in
  find (Mid.find id kn).pd_pure

let find_logic_definition kn ({ls_name = id} as ls) =
  let rec find = function
    | {d_news = s}::dl when not (Mid.mem id s) -> find dl
    | {d_node = Dlogic dl}::_ -> Some (List.assq ls dl)
    | _ -> None in
  find (Mid.find id kn).pd_pure
36

37 38 39 40 41 42 43 44 45 46 47
let apply_projection kn ls cs tl =
  let ts = match cs.ls_value with
    | Some { ty_node = Tyapp (ts,_) } -> ts
    | _ -> assert false in
  let pjl =
    try List.assq cs (find_constructors kn ts)
    with Not_found -> assert false in
  let find acc v = function
    | Some pj when ls_equal pj ls -> v
    | _ -> acc in
  List.fold_left2 find t_true tl pjl
48

49
let flat_case t bl =
Andrei Paskevich's avatar
Andrei Paskevich committed
50
  let mk_b b = let p,t = t_open_branch b in [p],t in
51 52
  let mk_case = t_case_close and mk_let = t_let_close_simp in
  Pattern.compile_bare ~mk_case ~mk_let [t] (List.map mk_b bl)
Andrei Paskevich's avatar
Andrei Paskevich committed
53

Andrei Paskevich's avatar
Andrei Paskevich committed
54 55
(* we destruct tuples, units, and singleton records *)
let destructible kn ty =
56 57
  let cl = match ty.ty_node with
    | Tyapp (ts, _) -> find_constructors kn ts
Andrei Paskevich's avatar
Andrei Paskevich committed
58
    | _ -> [] in
59
  match cl with
Andrei Paskevich's avatar
Andrei Paskevich committed
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
    | [ls,_] when is_fs_tuple ls -> Some ls
    | [{ls_args = [_]} as ls, _] -> Some ls
    | [{ls_args = []}  as ls, _] -> Some ls
    | _ -> None

(* we inline projections of destructed types *)
let find_inlineable kn ls = match ls.ls_args with
  | [arg] when destructible kn arg <> None ->
      begin match find_logic_definition kn ls with
      | Some def ->
          let res = open_ls_defn def in
          begin match (snd res).t_node with
          | Tvar _ | Tconst _
          | Tapp (_, [{t_node = Tvar _}]) -> Some res
          | Tcase ({t_node = Tvar _}, [bt]) ->
              begin match t_open_branch bt with
              | _, {t_node = Tvar _} -> Some res
              | _ -> None end
          | _ -> None end
      | _ -> None end
  | _ -> None

let unfold_inlineable kn ls tl ty = match find_inlineable kn ls with
  | Some (vl, e) ->
      let mt = List.fold_left2 (fun mt x y ->
        ty_match mt x.vs_ty (t_type y)) Mtv.empty vl tl in
      let mv = List.fold_right2 Mvs.add vl tl Mvs.empty in
      Some (t_ty_subst (oty_match mt e.t_ty ty) mv e)
  | None -> None

let rec add_quant kn (vl,tl,f) ({vs_ty = ty} as v) =
  match destructible kn ty with
    | Some ls ->
93
        let s = ty_match Mtv.empty (Opt.get ls.ls_value) ty in
94 95 96 97 98 99
        let mk_v ty = create_vsymbol (id_clone v.vs_name) (ty_inst s ty) in
        let nvl = List.map mk_v ls.ls_args in
        let t = fs_app ls (List.map t_var nvl) ty in
        let f = t_let_close_simp v t f in
        let tl = tr_map (t_subst_single v t) tl in
        List.fold_left (add_quant kn) (vl,tl,f) nvl
Andrei Paskevich's avatar
Andrei Paskevich committed
100
    | None ->
101 102
        (v::vl, tl, f)

Andrei Paskevich's avatar
Andrei Paskevich committed
103 104 105
let let_map fn env t1 tb =
  let x,t2,close = t_open_bound_cb tb in
  let t2 = fn (Mvs.add x t1 env) t2 in
106 107
  (* TODO/FIXME? convert (let x = if f then True else False in h)
     into (forall x. (x = True <-> f) -> h) ? *)
Andrei Paskevich's avatar
Andrei Paskevich committed
108 109 110 111 112 113 114
  t_let_simp t1 (close x t2)

let branch_map fn env t1 bl =
  let mk_b b =
    let p,t2,close = t_open_branch_cb b in close p (fn env t2) in
  t_case t1 (List.map mk_b bl)

115 116 117
let rec dive_to_constructor fn env t =
  let dive env t = dive_to_constructor fn env t in
  t_label_copy t (match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
118 119 120 121
    | Tvar x -> dive env (Mvs.find_exn Exit x env)
    | Tlet (t1,tb) -> let_map dive env t1 tb
    | Tcase (t1,bl) -> branch_map dive env t1 bl
    | Tif (f,t1,t2) -> t_if_simp f (dive env t1) (dive env t2)
122
    | Tapp (ls,tl) when ls.ls_constr > 0 -> fn env t ls tl
Andrei Paskevich's avatar
Andrei Paskevich committed
123 124
    | _ -> raise Exit)

Andrei Paskevich's avatar
Andrei Paskevich committed
125
let rec cs_equ env t1 t2 =
126 127 128 129 130 131 132 133
  if t_equal t1 t2 then t_true else
  let right cs1 tl1 env _t2 cs2 tl2 =
    if not (ls_equal cs1 cs2) then t_false else
    t_and_simp_l (List.map2 (cs_equ env) tl1 tl2) in
  let left t2 env _t1 cs1 tl1 =
    dive_to_constructor (right cs1 tl1) env t2 in
  try dive_to_constructor (left t2) env t1
  with Exit -> t_equ t1 t2
134

Andrei Paskevich's avatar
Andrei Paskevich committed
135 136 137 138
let rec eval_match kn stop env t =
  let stop = stop || Slab.mem Term.stop_split t.t_label in
  let eval env t = eval_match kn stop env t in
  t_label_copy t (match t.t_node with
139
    | Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
140
        cs_equ env (eval env t1) (eval env t2)
141 142
    | Tapp (ls, [t1]) when is_projection kn ls ->
        let t1 = eval env t1 in
143
        let fn _env _t2 cs tl = apply_projection kn ls cs tl in
Andrei Paskevich's avatar
Andrei Paskevich committed
144
        begin try dive_to_constructor fn env t1
145
        with Exit -> t_app ls [t1] t.t_ty end
Andrei Paskevich's avatar
Andrei Paskevich committed
146 147 148 149
    | Tapp (ls, tl) ->
        begin match unfold_inlineable kn ls tl t.t_ty with
        | Some t -> eval env t
        | None -> t_map (eval env) t
150
        end
151
    | Tlet (t1, tb2) ->
152
        let t1 = eval env t1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
153
        let_map eval env t1 tb2
Andrei Paskevich's avatar
Andrei Paskevich committed
154
    | Tcase (t1, bl1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
155
        let t1 = eval env t1 in
156 157
        let fn env t2 _cs _tl =
          eval env (Loc.try2 ?loc:t.t_loc flat_case t2 bl1) in
Andrei Paskevich's avatar
Andrei Paskevich committed
158
        begin try dive_to_constructor fn env t1
Andrei Paskevich's avatar
Andrei Paskevich committed
159
        with Exit -> branch_map eval env t1 bl1 end
160 161
    | Tquant (q, qf) ->
        let vl,tl,f,close = t_open_quant_cb qf in
Andrei Paskevich's avatar
Andrei Paskevich committed
162 163
        let vl,tl,f = if stop then List.rev vl,tl,f else
          List.fold_left (add_quant kn) ([],tl,f) vl in
164
        t_quant_simp q (close (List.rev vl) tl (eval env f))
165
    | _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
166 167 168
        t_map (eval env) t)

let eval_match kn t = eval_match kn false Mvs.empty t