Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit b6e2a7b6 authored by Andrei Paskevich's avatar Andrei Paskevich

Pdecl: split type declarations in chunks

Refinement code requires private types to reside in
separate program declarations. So we split type decls
into chunks where all non-free types are declared
separately and only constructible (Ddata) types are
kept together. The code preserves the original order
wherever possible.

Also, export ls_of_rs and fd_of_rs from Expr: these are
used everywhere in src/mlw anyway.

Also, remove some range/float-related "assert false".
parent 8d9366cc
......@@ -414,7 +414,7 @@ module Translate = struct
let not_g e = not (rs_ghost e) in
let pjl = itd.itd_fields in
let mfields = itd.itd_its.its_mfields in
let pv_equal_field rs = pv_equal (Opt.get rs.rs_field) in
let pv_equal_field rs = pv_equal (fd_of_rs rs) in
let get_mutable rs = List.exists (pv_equal_field rs) mfields in
match filter_ghost_params not_g get_mutable pjl with
| [is_mutable] -> not is_mutable
......@@ -695,7 +695,7 @@ module Translate = struct
List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
in
let drecord_fields ({rs_cty = rsc} as rs) =
(List.exists (pv_equal (Opt.get rs.rs_field)) s.its_mfields),
(List.exists (pv_equal (fd_of_rs rs)) s.its_mfields),
rs.rs_name,
ity rsc.cty_result
in
......
......@@ -210,6 +210,14 @@ let rs_of_ls ls =
let c = create_cty v_args [] [q] Mxs.empty Mpv.empty eff_empty ity in
mk_rs ls.ls_name c (RLls ls) None
let ls_of_rs rs = match rs.rs_logic with
| RLls ls -> ls
| _ -> invalid_arg "Expr.ls_of_rs"
let fd_of_rs rs = match rs.rs_field with
| Some fd -> fd
| _ -> invalid_arg "Expr.fd_of_rs"
(** {2 Program patterns} *)
type pat_ghost =
......
......@@ -65,6 +65,12 @@ val restore_rs : lsymbol -> rsymbol
val rs_ghost : rsymbol -> bool
val ls_of_rs : rsymbol -> lsymbol
(** raises [Invalid_argument] is [rs_logic] is not an [RLls] *)
val fd_of_rs : rsymbol -> pvsymbol
(** raises [Invalid_argument] is [rs_field] is [None] *)
(** {2 Program patterns} *)
type pat_ghost =
......
......@@ -65,8 +65,7 @@ let create_semi_constructor id s fdl pjl invl =
let ity = ity_app s tvl rgl in
let res = create_vsymbol (id_fresh "result") (ty_of_ity ity) in
let t = t_var res in
let get_pj p = match p.rs_logic with RLls s -> s | _ -> assert false in
let mk_q {pv_vs = v} p = t_equ (fs_app (get_pj p) [t] v.vs_ty) (t_var v) in
let mk_q {pv_vs = v} p = t_equ (fs_app (ls_of_rs p) [t] v.vs_ty) (t_var v) in
let q = create_post res (t_and_simp_l (List.map2 mk_q fdl pjl)) in
let eff = match ity.ity_node with
| Ityreg r -> eff_reset eff_empty (Sreg.singleton r)
......@@ -295,22 +294,24 @@ let get_syms node pure =
| PDexn xs -> syms_ity syms xs.xs_ity
| PDpure -> syms
let mk_decl_metas = let r = ref 0 in fun metas node pure ->
{ pd_node = node; pd_pure = pure; pd_meta = metas;
let mk_decl_meta = let r = ref 0 in fun meta node pure ->
{ pd_node = node;
pd_pure = pure;
pd_meta = meta;
pd_syms = get_syms node pure;
pd_news = get_news node pure;
pd_tag = (incr r; !r) }
let mk_decl = mk_decl_metas []
let mk_decl = mk_decl_meta []
let create_type_decl dl =
if dl = [] then invalid_arg "Pdecl.create_type_decl";
let add_itd ({itd_its = s} as itd) (abst,defn,rest,metas) =
let conv_itd ({itd_its = s} as itd) =
let {its_ts = {ts_name = {id_string = nm} as id} as ts} = s in
match itd.itd_fields, itd.itd_constructors, s.its_def with
| [], [], Alias _ ->
abst, defn, create_ty_decl ts :: rest, metas
| [], [], Range ir ->
| _, _, Alias _ ->
mk_decl (PDtype [itd]) [create_ty_decl ts]
| _, _, Range ir ->
let pj_id = id_derive (nm ^ "'int") id in
let pj_ls = create_fsymbol pj_id [ty_app ts []] ty_int in
let pj_decl = create_param_decl pj_ls in
......@@ -326,10 +327,10 @@ let create_type_decl dl =
let min_ic = Number.(int_const_dec (BigInt.to_string ir.ir_lower)) in
let min_defn = t_const (Number.ConstInt min_ic) ty_int in
let min_decl = create_logic_decl [make_ls_defn min_ls [] min_defn] in
let pure = [create_ty_decl ts; pj_decl; max_decl; min_decl] in
let meta = Theory.(meta_range, [MAts ts; MAls pj_ls]) in
let rest = pj_decl :: max_decl :: min_decl :: rest in
create_ty_decl ts :: abst, defn, rest, meta :: metas
| [], [], Float fmt ->
mk_decl_meta [meta] (PDtype [itd]) pure
| _, _, Float ff ->
let pj_id = id_derive (nm ^ "'real") id in
let pj_ls = create_fsymbol pj_id [ty_app ts []] ty_real in
let pj_decl = create_param_decl pj_ls in
......@@ -340,52 +341,74 @@ let create_type_decl dl =
(* create exponent digits attribute *)
let eb_id = id_derive (nm ^ "'eb") id in
let eb_ls = create_fsymbol eb_id [] ty_int in
let eb_defn = t_nat_const fmt.Number.fp_exponent_digits in
let eb_defn = t_nat_const ff.Number.fp_exponent_digits in
let eb_decl = create_logic_decl [make_ls_defn eb_ls [] eb_defn] in
(* create significand digits attribute *)
let sb_id = id_derive (nm ^ "'sb") id in
let sb_ls = create_fsymbol sb_id [] ty_int in
let sb_defn = t_nat_const fmt.Number.fp_significand_digits in
let sb_defn = t_nat_const ff.Number.fp_significand_digits in
let sb_decl = create_logic_decl [make_ls_defn sb_ls [] sb_defn] in
let pure = [create_ty_decl ts; pj_decl; iF_decl; eb_decl; sb_decl] in
let meta = Theory.(meta_float, [MAts ts; MAls pj_ls; MAls iF_ls]) in
let rest = pj_decl :: iF_decl :: eb_decl :: sb_decl :: rest in
create_ty_decl ts :: abst, defn, rest, meta :: metas
mk_decl_meta [meta] (PDtype [itd]) pure
| fl, _, NoDef when itd.itd_invariant <> [] ->
let ty = ty_app ts (List.map ty_var ts.ts_args) in
let u = create_vsymbol (id_fresh "self") ty in
let t = [t_var u] in
let get_ld s (ldd,sbs) = match s.rs_logic, s.rs_field with
| RLls s, Some v ->
create_param_decl s :: ldd,
Mvs.add v.pv_vs (t_app_infer s t) sbs
| _ -> assert false in
let proj, sbs = List.fold_right get_ld fl ([],Mvs.empty) in
let pr = create_prsymbol (id_derive (nm ^ "'invariant") id) in
let tl = [t_var u] in
let add_fd sbs s = let pj = ls_of_rs s in
Mvs.add (fd_of_rs s).pv_vs (t_app pj tl pj.ls_value) sbs in
let sbs = List.fold_left add_fd Mvs.empty fl in
let inv = t_subst sbs (t_and_simp_l itd.itd_invariant) in
let inv = t_forall_close [u] [] inv in
let inv = create_prop_decl Paxiom pr inv in
create_ty_decl ts :: abst, defn, proj @ inv :: rest, metas
let pr = create_prsymbol (id_derive (nm ^ "'invariant") id) in
let ax = create_prop_decl Paxiom pr (t_forall_close [u] [] inv) in
let add_fd s dl = create_param_decl (ls_of_rs s) :: dl in
let pure = create_ty_decl ts :: List.fold_right add_fd fl [ax] in
mk_decl (PDtype [itd]) pure
| fl, [], NoDef ->
let get_ld s ldd = match s.rs_logic with
| RLls s -> create_param_decl s :: ldd
| _ -> assert false in
let rest = List.fold_right get_ld fl rest in
create_ty_decl ts :: abst, defn, rest, metas
| fl, cl, NoDef ->
let add s f = Mpv.add (Opt.get f.rs_field) f s in
let mf = List.fold_left add Mpv.empty fl in
let get_fd s = match s.rs_logic with
| RLls s -> s | _ -> assert false in
let get_pj v = Opt.map get_fd (Mpv.find_opt v mf) in
let get_cs s = match s.rs_logic with
| RLls cs -> cs, List.map get_pj s.rs_cty.cty_args
| _ -> assert false in
abst, (ts, List.map get_cs cl) :: defn, rest, metas
| _ -> assert false (* impossible *)
let add_fd s dl = create_param_decl (ls_of_rs s) :: dl in
let pure = create_ty_decl ts :: List.fold_right add_fd fl [] in
mk_decl (PDtype [itd]) pure
| _, _, NoDef ->
(* we create here a temporary invalid declaration, just
to have pd_syms for the topological sorting later *)
mk_decl (PDtype [itd]) []
in
let abst,defn,rest,metas = List.fold_right add_itd dl ([],[],[],[]) in
let defn = if defn = [] then [] else [create_data_decl defn] in
mk_decl_metas metas (PDtype dl) (abst @ defn @ rest)
let hpd = Hid.create 3 in
let dl = List.map (fun itd ->
let id = itd.itd_its.its_ts.ts_name in
let d = conv_itd itd in
Hid.add hpd id d;
id, itd, d) dl in
let lvl = Hid.create 3 in
let rec count id = match Hid.find lvl id with
| n -> n | exception Not_found ->
begin match Hid.find hpd id with
| d -> Hid.add lvl id 0;
let n = Sid.fold (fun id n -> max (count id) n) d.pd_syms 0 in
let n = n - (n mod 2) + match d.pd_node with
| PDtype [{itd_constructors = _::_; itd_invariant = []}] -> 1
| _ -> 2 in
Hid.replace lvl id n; n
| exception Not_found -> 0 end in
let dl = List.map (fun (id,_,_ as d) -> d, count id) dl in
let rec insert dl d0 = match dl with
| d::dl when snd d0 < snd d -> d :: insert dl d0
| dl -> d0::dl in
let dl = List.fold_left insert [] dl in
let mk_data pdl ddl ldl = if ddl = [] then pdl else
mk_decl (PDtype ddl) [create_data_decl ldl] :: pdl in
let rec mount pdl ddl ldl = function
| ((_,_,d),l) :: dl when l mod 2 = 0 ->
mount (d :: mk_data pdl ddl ldl) [] [] dl
| ((_,d,_),_) :: dl ->
let add s f = Mpv.add (fd_of_rs f) f s in
let mf = List.fold_left add Mpv.empty d.itd_fields in
let get_pj v = Opt.map ls_of_rs (Mpv.find_opt v mf) in
let get_cs s = ls_of_rs s, List.map get_pj s.rs_cty.cty_args in
let ld = d.itd_its.its_ts, List.map get_cs d.itd_constructors in
mount pdl (d :: ddl) (ld :: ldl) dl
| [] -> mk_data pdl ddl ldl in
mount [] [] [] dl
(* TODO: share with Eliminate_definition *)
let rec t_insert hd t = match t.t_node with
......@@ -601,7 +624,7 @@ let print_its_defn fst fmt itd =
let print_regs pr fmt rl = if rl <> [] then
fprintf fmt "@ <%a>" (Pp.print_list Pp.comma pr) rl in
let print_field fmt f = fprintf fmt "%s%s%a%a : %a"
(if List.exists (pv_equal (Opt.get f.rs_field)) s.its_mfields
(if List.exists (pv_equal (fd_of_rs f)) s.its_mfields
then "mutable " else "") (if rs_ghost f then "ghost " else "")
print_rs f Pretty.print_id_labels f.rs_name
print_ity f.rs_cty.cty_result in
......@@ -621,6 +644,8 @@ let print_its_defn fst fmt itd =
let print_defn fmt () =
match s.its_def, itd.itd_fields, itd.itd_constructors with
| Alias ity, _, _ -> fprintf fmt " = %a" print_ity ity
| Range _ir, _, _ -> fprintf fmt " = <range ...>" (* TODO *)
| Float _ff, _, _ -> fprintf fmt " = <float ...>" (* TODO *)
| NoDef, [], [] when not s.its_mutable -> ()
| NoDef, fl, [] -> fprintf fmt " = private%s { %a }"
(if s.its_mutable && s.its_mfields = [] then " mutable" else "")
......@@ -630,11 +655,10 @@ let print_its_defn fst fmt itd =
(if s.its_mutable && s.its_mfields = [] then " mutable" else "")
(Pp.print_list Pp.semi print_field) fl
| NoDef, fl, cl ->
let add s f = Mpv.add (Opt.get f.rs_field) f s in
let add s f = Mpv.add (fd_of_rs f) f s in
let mf = List.fold_left add Mpv.empty fl in
fprintf fmt " =%a" (Pp.print_list Pp.nothing (print_constr mf)) cl
| Range _, _, _ -> assert false (* TODO *)
| Float _, _, _ -> assert false (* TODO *) in
in
let print_inv fmt f = fprintf fmt
"@\n@ invariant { %a }" Pretty.print_term f in
fprintf fmt "@[<hov 2>%s %a%a%a%a%a%a@]"
......
......@@ -91,7 +91,7 @@ and pdecl_node = private
and meta_decl = Theory.meta * Theory.meta_arg list
val create_type_decl : its_defn list -> pdecl
val create_type_decl : its_defn list -> pdecl list
val create_let_decl : let_defn -> pdecl
......
......@@ -503,7 +503,7 @@ let rec eval_expr env (e : expr) : result =
| Eassign l ->
List.iter
(fun (pvs,rs,value) ->
let fld = Opt.get rs.rs_field in
let fld = fd_of_rs rs in
let value = get_pvs env value in
match get_pvs env pvs with
| Vconstr(cstr,args) ->
......
......@@ -289,7 +289,8 @@ let add_pdecl_no_logic uc d =
let add_pdecl_raw ?(warn=true) uc d =
let uc = add_pdecl_no_logic uc d in
let th = List.fold_left (add_decl ~warn) uc.muc_theory d.pd_pure in
let th = List.fold_left (fun th (m,l) -> Theory.add_meta th m l) th d.pd_meta in
let add_meta th (m,l) = Theory.add_meta th m l in
let th = List.fold_left add_meta th d.pd_meta in
{ uc with muc_theory = th }
(** {2 Builtin symbols} *)
......@@ -327,9 +328,9 @@ let tuple_module = Hint.memo 17 (fun n ->
let unit_module =
let uc = empty_module dummy_env (id_fresh "Unit") ["why3";"Unit"] in
let uc = use_export uc (tuple_module 0) in
let add uc d = add_pdecl_raw ~warn:false uc d in
let td = create_alias_decl (id_fresh "unit") [] ity_unit in
let d = create_type_decl [td] in
close_module (add_pdecl_raw ~warn:false uc d)
close_module (List.fold_left add uc (create_type_decl [td]))
let create_module env ?(path=[]) n =
let m = empty_module env n path in
......@@ -628,26 +629,20 @@ let mk_record_invariant d s =
let inv = t_subst sbs (t_and_simp_l d.itd_invariant) in
t_forall_close [u] [] inv
(* Mário: commented out this function *)
let ls_of_rs rs = match rs.rs_logic with
| RLls ls -> ls
| _ -> assert false
let clone_type_record cl s d s' d' =
let id = s.its_ts.ts_name in
let fields' = Hstr.create 16 in
let add_field' ({rs_field = pj'} as rs') =
let pj' = Opt.get pj' in
let add_field' rs' = let pj' = fd_of_rs rs' in
Hstr.add fields' pj'.pv_vs.vs_name.id_string rs' in
List.iter add_field' d'.itd_fields;
(* check if fields from former type are also declared in the new type *)
let match_pj ({rs_field = pj} as rs) = let pj = Opt.get pj in
let match_pj rs = let pj = fd_of_rs rs in
let pj_str = pj.pv_vs.vs_name.id_string in
let pj_ity = clone_ity cl pj.pv_ity in
let pj_ght = pj.pv_ghost in
let rs' = try Hstr.find fields' pj_str
with Not_found -> raise (BadInstance id) in
let pj' = Opt.get rs'.rs_field in
let pj' = fd_of_rs rs' in
let pj'_ity = pj'.pv_ity in
let pj'_ght = pj'.pv_ghost in
if not (ity_equal pj_ity pj'_ity && (pj_ght || not pj'_ght)) then
......@@ -676,16 +671,16 @@ let clone_type_decl inst cl tdl kn =
List.iter2 (cl_save_rs cl) d.itd_fields itd.itd_fields;
Hits.add htd s (Some itd) in
(* alias *)
match s.its_def with
| Alias ty ->
if s.its_def <> NoDef then begin
if cloned then raise (CannotInstantiate id);
let def = conv_ity alg ty in
let itd = create_alias_decl id' ts.ts_args def in
let itd = match s.its_def with
| Alias ty -> create_alias_decl id' ts.ts_args (conv_ity alg ty)
| Range ir -> create_range_decl id' ir
| Float ff -> create_float_decl id' ff
| NoDef -> assert false (* never *) in
cl.ts_table <- Mts.add ts itd.itd_its cl.ts_table;
save_itd itd
| Range _ -> assert false (* TODO *)
| Float _ -> assert false (* TODO *)
| NoDef ->
end else
(* abstract *)
if s.its_private && cloned then begin
(* FIXME: currently, we cannot refine a block of mutual types *)
......@@ -725,7 +720,7 @@ let clone_type_decl inst cl tdl kn =
d.itd_invariant = [] then begin
if cloned then raise (CannotInstantiate id);
let conv_fd m fd =
let v = Opt.get fd.rs_field in Mpv.add v (conv_pj v) m in
let v = fd_of_rs fd in Mpv.add v (conv_pj v) m in
let fldm = List.fold_left conv_fd Mpv.empty d.itd_fields in
let conv_pj pj = match Mpv.find_opt pj fldm with
| Some pj' -> true, pj' | None -> false, conv_pj pj in
......@@ -744,7 +739,7 @@ let clone_type_decl inst cl tdl kn =
(* flat record *)
if cloned then raise (CannotInstantiate id);
let mfld = Spv.of_list s.its_mfields in
let pjl = List.map (fun fd -> Opt.get fd.rs_field) d.itd_fields in
let pjl = List.map fd_of_rs d.itd_fields in
let fdl = List.map (fun v -> Spv.mem v mfld, conv_pj v) pjl in
let inv =
if d.itd_invariant = [] then [] else
......@@ -953,8 +948,8 @@ let clone_pdecl inst cl uc d = match d.pd_node with
| PDtype tdl ->
let tdl, vcl = clone_type_decl inst cl tdl uc.muc_known in
if tdl = [] then List.fold_left add_vc uc vcl else
let d = create_type_decl tdl in
add_pdecl ~warn:false ~vc:false uc d
let add uc d = add_pdecl ~warn:false ~vc:false uc d in
List.fold_left add uc (create_type_decl tdl)
| PDlet (LDsym (rs, c)) when Mrs.mem rs inst.mi_rs ->
(* refine only [val] symbols *)
if c.c_node <> Cany then raise (BadInstance rs.rs_name);
......
......@@ -17,9 +17,6 @@ open Ity
open Expr
open Pdecl
let ls_of_rs s = match s.rs_logic with
RLls ls -> ls | _ -> assert false
let ls_valid =
let v = create_tvsymbol (id_fresh "a") in
create_psymbol (id_fresh "valid") [ty_var v]
......@@ -123,7 +120,7 @@ let add_gl_cap kn v =
let sbs = ts_match_args s.its_ts tl in
if s.its_nonfree then if s.its_fragile then (* breakable record *)
let add_field m f =
let vf = Opt.get f.rs_field in
let vf = fd_of_rs f in
let ty = Ty.ty_inst sbs vf.pv_vs.vs_ty in
let leaf = fs_app (ls_of_rs f) [leaf] ty in
Mls.add (ls_of_rs f) (down stem leaf ty) m in
......@@ -134,13 +131,13 @@ let add_gl_cap kn v =
mkP n
else (* unbreakable record *)
let add_field m f =
let vf = Opt.get f.rs_field in
let vf = fd_of_rs f in
let ty = Ty.ty_inst sbs vf.pv_vs.vs_ty in
let leaf = fs_app (ls_of_rs f) [leaf] ty in
Mls.add (ls_of_rs f) (down stem leaf ty) m in
mkR (List.fold_left add_field Mls.empty d.itd_fields)
else if List.length d.itd_constructors == 1 then (* record type *)
let add_field m f = Mpv.add (Opt.get f.rs_field) (ls_of_rs f) m in
let add_field m f = Mpv.add (fd_of_rs f) (ls_of_rs f) m in
let pjm = List.fold_left add_field Mpv.empty d.itd_fields in
let add_constr m c =
let inst f = Ty.ty_inst sbs f.pv_vs.vs_ty in
......@@ -327,7 +324,7 @@ let add_var kn pins vl v =
if s.its_nonfree then if s.its_fragile then (* breakable record *)
let bn = v.vs_name.id_string in
let add_field (m,mv) f =
let vf = Opt.get f.rs_field in
let vf = fd_of_rs f in
let ty = Ty.ty_inst sbs vf.pv_vs.vs_ty in
let nm = bn ^ "_" ^ f.rs_name.id_string in
let v = create_vsymbol (id_fresh nm) ty in
......@@ -343,7 +340,7 @@ let add_var kn pins vl v =
mkP n
else (* unbreakable record *)
let add_field m f =
let vf = Opt.get f.rs_field in
let vf = fd_of_rs f in
let ty = Ty.ty_inst sbs vf.pv_vs.vs_ty in
Mls.add (ls_of_rs f) (down ty) m in
mkR (List.fold_left add_field Mls.empty d.itd_fields)
......
......@@ -32,8 +32,6 @@ let no_eval = Debug.register_flag "vc_no_eval"
let case_split = Ident.create_label "case_split"
let add_case t = t_label_add case_split t
let ls_of_rs s = match s.rs_logic with RLls ls -> ls | _ -> assert false
let clone_vs v = create_vsymbol (id_clone v.vs_name) v.vs_ty
let clone_pv v = clone_vs v.pv_vs
......@@ -533,7 +531,7 @@ let rec k_expr env lps ({e_loc = loc} as e) res xmap =
if Sreg.is_empty cv then k_unit res else
(* compute the write effect *)
let add wr (r,f,v) =
let f = Opt.get f.rs_field in
let f = fd_of_rs f in
let r = match r.pv_ity.ity_node with
| Ityreg r -> r | _ -> assert false in
Mreg.change (function
......@@ -1000,7 +998,7 @@ let rec havoc kn wr regs t ity fl =
let wfs = Mreg.find_def Mpv.empty r wr in
let nt = Mreg.find r regs in
let field rs fl =
let fd = Opt.get rs.rs_field in
let fd = fd_of_rs rs in
match Mpv.find_opt fd wfs with
| Some None -> fl
| Some (Some {pv_vs = v}) ->
......
......@@ -929,8 +929,8 @@ let add_types muc tdl =
Mstr.iter (visit ~alias:Mstr.empty ~alg:Mstr.empty) def;
let tdl = List.map (fun d -> Hstr.find htd d.td_ident.id_str) tdl in
let d = create_type_decl tdl in
add_pdecl ~vc:true muc d
let add muc d = add_pdecl ~vc:true muc d in
List.fold_left add muc (create_type_decl tdl)
let tyl_of_params {muc_theory = tuc} pl =
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment