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/

programs: builtin exn type, variants with inlined lt_nat

parent 286a3b89
......@@ -38,7 +38,7 @@ let test_not_1 () =
let test_not_2 () =
{ x <= 0 }
while not (!x = 0) do invariant { !x <= 0 } incr x done
while not (!x = 0) do invariant { x <= 0 } incr x done
{ x = 0 }
let test_all_1 () =
......
module M
exception Exception of int
exception Exception int
use import module stdlib.Ref
parameter t : ref int
......
module M
use import int.Int
use import module stdlib.Ref
exception Break
let f (n : int) : int =
......@@ -8,7 +11,7 @@ let f (n : int) : int =
try
while (!i > 0) do
invariant { true }
variant { !i }
variant { i }
if (!i <= 10) then raise Break;
i := !i - 1
done
......
......@@ -1190,8 +1190,8 @@ opt_raises:
opt_variant:
| /* epsilon */ { None }
| VARIANT annotation { Some ($2, id_lt_nat ()) }
| VARIANT annotation WITH lqualid { Some ($2, $4) }
| VARIANT annotation { Some ($2, None) }
| VARIANT annotation WITH lqualid { Some ($2, Some $4) }
;
opt_cast:
......
......@@ -155,7 +155,7 @@ type assertion_kind = Aassert | Aassume | Acheck
type lazy_op = LazyAnd | LazyOr
type variant = lexpr * qualid
type variant = lexpr * qualid option
type loop_annotation = {
loop_invariant : lexpr option;
......
......@@ -3,6 +3,6 @@ X refs -> mutable types
X loadpath: how to retrieve program files? (cannot use "env")
o what about pervasives old, at, label, exn, unit = (), lt_nat
o what about pervasives old, at, label, unit = (), lt_nat
in particular, how to prevent old and at from being used in programs?
......@@ -89,16 +89,6 @@ let add_pervasives uc =
in
add_ty_decl uc [ts, Decl.Tabstract]
let create_module n =
let uc = Theory.create_theory n in
(* let uc = add_pervasives uc in *)
{ uc_name = id_register n;
uc_th = uc;
uc_decls = [];
uc_import = [empty_ns];
uc_export = [empty_ns];
}
let open_namespace uc = match uc.uc_import with
| ns :: _ -> { uc with
uc_th = Theory.open_namespace uc.uc_th;
......@@ -145,6 +135,20 @@ let add_logic_decl d uc =
let th = Typing.with_tuples Theory.add_decl uc.uc_th d in
{ uc with uc_th = th }
let ls_Exit = create_lsymbol (id_fresh "%Exit") [] (Some ty_exn)
let create_module n =
let uc = Theory.create_theory n in
(* let uc = add_pervasives uc in *)
let m = {
uc_name = id_register n;
uc_th = uc;
uc_decls = [];
uc_import = [empty_ns];
uc_export = [empty_ns]; }
in
add_esymbol ls_Exit m
(** Modules *)
type t = {
......
......@@ -64,7 +64,7 @@ and dtype_c =
and dbinder = ident * Denv.dty * dtype_v
type dvariant = Denv.dterm * Term.lsymbol
type dvariant = Denv.dterm * Term.lsymbol option
type dloop_annotation = {
dloop_invariant : Denv.dfmla option;
......@@ -109,7 +109,7 @@ and dtriple = dpre * dexpr * dpost
(*****************************************************************************)
(* phase 2: removal of destructive types *)
type variant = Term.term * Term.lsymbol
type variant = Term.term * Term.lsymbol option
type reference = R.t
......@@ -153,7 +153,7 @@ type loop_annotation = {
type label = Term.vsymbol
type irec_variant = ivsymbol * Term.term * Term.lsymbol
type irec_variant = ivsymbol * Term.term * Term.lsymbol option
type ipattern = {
ipat_pat : Term.pattern;
......@@ -205,7 +205,7 @@ and itriple = pre * iexpr * post
(*****************************************************************************)
(* phase 3: effect inference *)
type rec_variant = pvsymbol * Term.term * Term.lsymbol
type rec_variant = pvsymbol * Term.term * Term.lsymbol option
type pattern = {
ppat_pat : Term.pattern;
......
......@@ -59,6 +59,9 @@ let model_type ty = match ty.ty_node with
(* types *)
let ts_exn = Ty.create_tysymbol (id_fresh "exn") [] None
let ty_exn = Ty.ty_app ts_exn []
let ts_arrow =
let v = List.map (fun s -> create_tvsymbol (Ident.id_fresh s)) ["a"; "b"] in
Ty.create_tysymbol (Ident.id_fresh "arrow") v None
......
......@@ -30,6 +30,9 @@ val is_mutable_ty : ty -> bool
val ts_arrow : tysymbol
val ts_exn : tysymbol
val ty_exn : ty
(* program types *)
module rec T : sig
......
......@@ -232,7 +232,7 @@ let dexception env qid =
let sl = Typing.string_list_of_qualid [] qid in
let loc = Typing.qloc qid in
let _, _, ty as r = specialize_exception loc sl env.uc in
let ty_exn = dty_app (find_ts env.uc "exn", []) in
let ty_exn = dty_app (ts_exn, []) in
if not (Denv.unify ty ty_exn) then
errorm ~loc
"this expression has type %a, but is expected to be an exception"
......@@ -305,16 +305,23 @@ let rec add_local_pat env p = match p.dp_node with
| Denv.Por (p, q) -> add_local_pat (add_local_pat env p) q
let dvariant env (l, p) =
let s, _ = Typing.specialize_psymbol p (theory_uc env.uc) in
let loc = Typing.qloc p in
begin match s.ls_args with
| [t1; t2] when Ty.ty_equal t1 t2 ->
()
| _ ->
errorm ~loc "predicate %s should be a binary relation"
s.ls_name.id_string
end;
dterm env.denv l, s
let t = dterm env.denv l in
match p with
| None ->
if not (Denv.unify t.dt_ty (dty_int env.uc)) then
errorm ~loc:l.pp_loc "variant should have type int";
t, None
| Some p ->
let s, _ = Typing.specialize_psymbol p (theory_uc env.uc) in
let loc = Typing.qloc p in
begin match s.ls_args with
| [t1; t2] when Ty.ty_equal t1 t2 ->
()
| _ ->
errorm ~loc "predicate %s should be a binary relation"
s.ls_name.id_string
end;
t, Some s
let dloop_annotation env a =
{ dloop_invariant = option_map (dfmla env.denv) a.Ptree.loop_invariant;
......@@ -583,10 +590,12 @@ let post env ((ty, f), ql) =
let variant loc env (t, ps) =
let t = Denv.term env t in
match ps.ls_args with
| [t1; _] when Ty.ty_equal t1 t.t_ty ->
match ps with
| None ->
t, ps
| Some { ls_args = [t1; _] } when Ty.ty_equal t1 t.t_ty ->
t, ps
| [t1; _] ->
| Some { ls_args = [t1; _] } ->
errorm ~loc "@[variant has type %a, but is expected to have type %a@]"
Pretty.print_ty t.t_ty Pretty.print_ty t1
| _ ->
......@@ -873,9 +882,14 @@ and iletrec gl env dl =
let check_no_variant (_,_,var,(_,e,_)) = if var <> None then error e in
List.iter check_no_variant r
| (_, _, Some (_, _, ps), _) :: r ->
let r_equal r1 r2 = match r1, r2 with
| None, None -> true
| Some ls1, Some ls2 -> ls_equal ls1 ls2
| _ -> false
in
let check_variant (_,_,var,(_,e,_)) = match var with
| None -> error e
| Some (_, _, ps') -> if not (ls_equal ps ps') then
| Some (_, _, ps') -> if not (r_equal ps ps') then
errorm ~loc:e.iexpr_loc
"variants must share the same order relation"
in
......@@ -1278,7 +1292,14 @@ and letrec gl env dl = (* : env * recfun list *)
let c = Mvs.find i.i_pgm m in
let c = match decvar, var with
| Some phi0, Some (_, phi, r) ->
let decphi = f_app r [phi; t_var phi0] in
let decphi = match r with
| None -> (* 0 <= phi0 and phi < phi0 *)
f_and (f_app (find_ls gl "infix <=")
[t_int_const "0"; t_var phi0])
(f_app (find_ls gl "infix <") [phi; t_var phi0])
| Some r ->
f_app r [phi; t_var phi0]
in
{ c with c_pre = f_and decphi c.c_pre }
| _ ->
c
......@@ -1444,7 +1465,7 @@ let add_exception loc x ty uc =
try
let tyl = match ty with None -> [] | Some ty -> [ty] in
let id = id_user x loc in
let ls = create_lsymbol id tyl (Some (ty_app (find_ts uc "exn") [])) in
let ls = create_lsymbol id tyl (Some (ty_app ts_exn [])) in
add_esymbol ls uc
with ClashSymbol _ ->
errorm ~loc "clash with previous exception %s" x
......
......@@ -227,7 +227,12 @@ let while_post_block env inv var lab e =
let decphi = match var with
| None ->
f_true
| Some (phi, r) ->
| Some (phi, None) ->
let old_phi = term_at env lab phi in
(* 0 <= old_phi and phi < old_phi *)
wp_and (f_app (find_ls env "infix <=") [t_int_const "0"; old_phi])
(f_app (find_ls env "infix <") [phi; old_phi])
| Some (phi, Some r) ->
f_app r [phi; term_at env lab phi]
in
let ql = default_exns_post e.expr_effect in
......
......@@ -9,10 +9,6 @@ theory Prelude
logic at 'a label_ : 'a
logic old 'a : 'a
type exn
(* logic lt_nat (x y:int) = 0 <= y and x < y *)
end
......
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