Skip to content

GitLab

why3
why3
Commit b12336ca authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

cosmetic changes re "partial"

parent 1db0fc87
Hide whitespace changes
Inline Side-by-side
Showing with 110 additions and 101 deletions
bench/typing/bad/partial_function.mlw
View file @ b12336ca
val function partial f (x:int) : unit
\ No newline at end of file
val partial function f (x:int) : unit
bench/typing/bad/partial_ghost.mlw deleted 100644 → 0
View file @ 1db0fc87
val ghost partial f () : int
\ No newline at end of file
bench/typing/bad/partial_lemma.mlw
View file @ b12336ca
let lemma partial f (x:int)
let partial lemma f (x:int)
ensures { true }
= ()
\ No newline at end of file
= ()
src/mlw/dexpr.ml
View file @ b12336ca
......@@ -926,10 +926,10 @@ let check_spec inr dsp ecty ({e_loc = loc} as e) =
if check_ue && bad_raise ueff eeff then Loc.errorm ?loc
"this@ expression@ does@ not@ raise@ exception@ %a"
print_xs (Sxs.choose (Sxs.diff ueff.eff_raises eeff.eff_raises));
if check_ue && (diverges ueff.eff_oneway) && not (diverges eeff.eff_oneway)
then Loc.errorm ?loc "this@ expression@ does@ not@ diverge";
if check_ue && (partial ueff.eff_oneway) && (ghostifiable eeff.eff_oneway)
then Loc.errorm ?loc "this@ expression's@ termination@ is@ not@ partial";
if check_ue && diverges ueff.eff_oneway && not (diverges eeff.eff_oneway)
then Loc.errorm ?loc "this@ expression@ does@ not@ diverge";
if check_ue && partial ueff.eff_oneway && total eeff.eff_oneway
then Loc.errorm ?loc "this@ expression@ does@ not@ diverge@ or@ fail";
(* check that every computed effect is listed *)
if check_rw && bad_read eeff ueff then Loc.errorm ?loc
"this@ expression@ depends@ on@ variable@ %a,@ \
......
src/mlw/expr.ml
View file @ b12336ca
......@@ -1176,13 +1176,13 @@ let print_rs fmt s =
let print_rs_head fmt s = fprintf fmt "%s%s%s%a%a"
(if s.rs_cty.cty_effect.eff_ghost then "ghost " else "")
(if partial s.rs_cty.cty_effect.eff_oneway then "partial " else "")
(match s.rs_logic with
| RLnone -> ""
| RLpv _ -> "function "
| RLls {ls_value = None} -> "predicate "
| RLls _ -> "function "
| RLlemma -> "lemma ")
(if partial s.rs_cty.cty_effect.eff_oneway then "partial " else "")
print_rs s print_id_attrs (id_of_rs s)
let print_invariant fmt fl =
......
src/mlw/ity.ml
View file @ b12336ca
......@@ -868,30 +868,31 @@ exception IllegalAssign of region * region * region
exception ImpureVariable of tvsymbol * ity
exception GhostDivergence
type termination_status =
| Ghostifiable
(* termination status *)
type oneway =
| Total
| Partial
| Diverges
let ghostifiable status = (status = Ghostifiable)
let total status = (status = Total)
let partial status = (status = Partial)
let diverges status = (status = Diverges)
let termination_union t1 t2 = match (t1, t2) with
| Ghostifiable, Ghostifiable -> Ghostifiable
let oneway_union t1 t2 = match t1, t2 with
| Total, Total -> Total
| _, Diverges | Diverges, _ -> Diverges
| _ -> Partial
type effect = {
eff_reads : Spv.t; (* known variables *)
eff_writes : Spv.t Mreg.t; (* writes to fields *)
eff_taints : Sreg.t; (* ghost code writes *)
eff_covers : Sreg.t; (* surviving writes *)
eff_resets : Sreg.t; (* locked by covers *)
eff_raises : Sxs.t; (* raised exceptions *)
eff_spoils : Stv.t; (* immutable tyvars *)
eff_oneway : termination_status; (* non-termination *)
eff_ghost : bool; (* ghost status *)
eff_reads : Spv.t; (* known variables *)
eff_writes : Spv.t Mreg.t; (* writes to fields *)
eff_taints : Sreg.t; (* ghost code writes *)
eff_covers : Sreg.t; (* surviving writes *)
eff_resets : Sreg.t; (* locked by covers *)
eff_raises : Sxs.t; (* raised exceptions *)
eff_spoils : Stv.t; (* immutable tyvars *)
eff_oneway : oneway; (* non-termination *)
eff_ghost : bool; (* ghost status *)
}
let eff_empty = {
......@@ -902,7 +903,7 @@ let eff_empty = {
eff_resets = Sreg.empty;
eff_raises = Sxs.empty;
eff_spoils = Stv.empty;
eff_oneway = Ghostifiable;
eff_oneway = Total;
eff_ghost = false;
}
......@@ -920,7 +921,7 @@ let eff_equal e1 e2 =
let eff_pure e =
Mreg.is_empty e.eff_writes &&
Sxs.is_empty e.eff_raises &&
ghostifiable e.eff_oneway
total e.eff_oneway
let check_writes {eff_writes = wrt} pvs =
if not (Mreg.is_empty wrt) then Spv.iter (fun v ->
......@@ -954,12 +955,12 @@ let reset_taints e =
let eff_ghostify gh e =
if not gh || e.eff_ghost then e else
if (not (ghostifiable e.eff_oneway)) then raise GhostDivergence else
if not (total e.eff_oneway) then raise GhostDivergence else
reset_taints { e with eff_ghost = true }
let eff_ghostify_weak gh e =
if not gh || e.eff_ghost then e else
if not (ghostifiable e.eff_oneway && Sxs.is_empty e.eff_raises) then e else
if not (total e.eff_oneway && Sxs.is_empty e.eff_raises) then e else
if not (Sreg.equal e.eff_taints (visible_writes e)) then e else
(* it is not enough to catch BadGhostWrite from eff_ghostify below,
because e may not have in eff_reads the needed visible variables
......@@ -968,11 +969,12 @@ let eff_ghostify_weak gh e =
eff_ghostify gh e
let eff_partial e =
if diverges e.eff_oneway || partial e.eff_oneway then e
else if e.eff_ghost then raise GhostDivergence else
if diverges e.eff_oneway || partial e.eff_oneway then e else
if e.eff_ghost then raise GhostDivergence else
{ e with eff_oneway = Partial }
let eff_diverge e = if diverges e.eff_oneway then e else
let eff_diverge e =
if diverges e.eff_oneway then e else
if e.eff_ghost then raise GhostDivergence else
{ e with eff_oneway = Diverges }
......@@ -1096,7 +1098,7 @@ let eff_assign asl =
eff_resets = resets;
eff_raises = Sxs.empty;
eff_spoils = Stv.empty;
eff_oneway = Ghostifiable;
eff_oneway = Total;
eff_ghost = ghost } in
(* verify that we can rebuild every value *)
check_writes effect reads;
......@@ -1139,7 +1141,7 @@ let eff_union e1 e2 = {
eff_resets = Sreg.union e1.eff_resets e2.eff_resets;
eff_raises = Sxs.union e1.eff_raises e2.eff_raises;
eff_spoils = Stv.union e1.eff_spoils e2.eff_spoils;
eff_oneway = termination_union e1.eff_oneway e2.eff_oneway;
eff_oneway = oneway_union e1.eff_oneway e2.eff_oneway;
eff_ghost = e1.eff_ghost && e2.eff_ghost }
let eff_union e1 e2 =
......@@ -1500,9 +1502,9 @@ let cty_exec ({cty_effect = eff} as c) =
in the resulting pvsymbol. Thus, we have to forbid all effects,
including allocation. TODO/FIXME: we should probably forbid
the rest of the signature to contain regions at all. *)
if (diverges eff.eff_oneway) then Loc.errorm
if diverges eff.eff_oneway then Loc.errorm
"This function may not terminate, it cannot be used as pure";
if (partial eff.eff_oneway) then Loc.errorm
if partial eff.eff_oneway then Loc.errorm
"This function may fail, it cannot be used as pure";
if not (eff_pure eff && Sreg.is_empty eff.eff_resets) then Loc.errorm
"This function has side effects, it cannot be used as pure";
......
src/mlw/ity.mli
View file @ b12336ca
......@@ -339,25 +339,26 @@ exception IllegalAssign of region * region * region
exception ImpureVariable of tvsymbol * ity
exception GhostDivergence
type termination_status =
| Ghostifiable
(* termination status *)
type oneway =
| Total
| Partial
| Diverges
val ghostifiable : termination_status -> bool
val partial : termination_status -> bool
val diverges : termination_status -> bool
val total : oneway -> bool
val partial : oneway -> bool
val diverges : oneway -> bool
type effect = private {
eff_reads : Spv.t; (* known variables *)
eff_writes : Spv.t Mreg.t; (* writes to fields *)
eff_taints : Sreg.t; (* ghost code writes *)
eff_covers : Sreg.t; (* surviving writes *)
eff_resets : Sreg.t; (* locked by covers *)
eff_raises : Sxs.t; (* raised exceptions *)
eff_spoils : Stv.t; (* immutable tyvars *)
eff_oneway : termination_status; (* non-termination *)
eff_ghost : bool; (* ghost status *)
eff_reads : Spv.t; (* known variables *)
eff_writes : Spv.t Mreg.t; (* writes to fields *)
eff_taints : Sreg.t; (* ghost code writes *)
eff_covers : Sreg.t; (* surviving writes *)
eff_resets : Sreg.t; (* locked by covers *)
eff_raises : Sxs.t; (* raised exceptions *)
eff_spoils : Stv.t; (* immutable tyvars *)
eff_oneway : oneway; (* non-termination *)
eff_ghost : bool; (* ghost status *)
}
val eff_empty : effect
......
src/mlw/pdecl.ml
View file @ b12336ca
......@@ -541,8 +541,7 @@ let create_let_decl ld =
Loc.error ?loc:ls.ls_name.id_loc (Decl.NoTerminationProof ls) in
let is_trusted_rec = match ld with
| LDrec ({rec_sym = {rs_logic = RLls ls; rs_cty = c}; rec_varl = []}::_)
when ghostifiable c.cty_effect.eff_oneway ->
abst = [] || fail_trusted_rec ls
when total c.cty_effect.eff_oneway -> abst = [] || fail_trusted_rec ls
| _ -> false in
let defn = if defn = [] then [] else
let dl = List.map (fun (s,vl,t) -> make_ls_defn s vl t) defn in
......
src/mlw/pmodule.ml
View file @ b12336ca
......@@ -1057,7 +1057,7 @@ let clone_pdecl inst cl uc d = match d.pd_node with
end;
begin
match cty.cty_effect.eff_oneway, rs'.rs_cty.cty_effect.eff_oneway with
| _, Ghostifiable | Diverges, _ | Partial, Partial -> ()
| _, Total | Diverges, _ | Partial, Partial -> ()
| _ -> raise (CloneDivergence (rs.rs_name, rs'.rs_name))
end;
cl.rs_table <- Mrs.add rs rs' cl.rs_table;
......@@ -1246,5 +1246,5 @@ let () = Exn_printer.register (fun fmt e -> match e with
| CloneDivergence (iv, il) -> Format.fprintf fmt
"Cannot instantiate symbol %a with symbol %a \
that has worse termination status"
print_id iv print_id il
print_id iv print_id il
| _ -> raise e)
src/parser/parser.mly
View file @ b12336ca
......@@ -108,23 +108,28 @@
| Pwild -> sp
| _ -> { sp with sp_post = List.map apply sp.sp_post }
let apply_partial part sp =
if part
then { sp with sp_partial = true }
else sp
let apply_partial_ed e =
match e with
| Efun (bl, op, m, s, ex) ->
Efun (bl, op, m, apply_partial true s, ex)
| Eany (pl, rsk, op, m, s) ->
Eany (pl, rsk, op, m, apply_partial true s)
| _ -> assert false
let apply_partial_e part e =
if part
then { e with expr_desc = apply_partial_ed e.expr_desc }
else e
type partial =
| Regular
| Partial
| Ghost
let ghost part = (part = Ghost)
let apply_partial_sp part sp =
if part <> Partial then sp else
{ sp with sp_partial = true }
let apply_partial part e =
if part <> Partial then e else
let ed = match e.expr_desc with
| Efun (_::_ as bl, op, m, s, ex) ->
Efun (bl, op, m, apply_partial_sp part s, ex)
| Eany (_::_ as pl, rsk, op, m, s) ->
Eany (pl, rsk, op, m, apply_partial_sp part s)
| _ ->
Loc.errorm ~loc:e.expr_loc
"this expression cannot be declared partial" in
{ e with expr_desc = ed }
let we_attr = Ident.create_attribute "expl:witness existence"
......@@ -747,18 +752,26 @@ numeral:
(* Program declarations *)
prog_decl:
| VAL ghost kind partial attrs(lident_rich) mk_expr(val_defn)
{ Dlet (add_model_trace_attr $5, $2, $3, apply_partial_e $4 $6) }
| LET ghost kind partial attrs(lident_rich) mk_expr(fun_defn)
{ Dlet ($5, $2, $3, apply_partial_e $4 $6) }
| LET ghost kind attrs(lident_rich) const_defn { Dlet ($4, $2, $3, $5) }
| LET REC with_list1(rec_defn) { Drec $3 }
| EXCEPTION attrs(uident_nq) { Dexn ($2, PTtuple [], Ity.MaskVisible) }
| EXCEPTION attrs(uident_nq) return { Dexn ($2, fst $3, snd $3) }
| VAL ghost kind attrs(lident_rich) mk_expr(val_defn)
{ Dlet (add_model_trace_attr $4, ghost $2, $3, apply_partial $2 $5) }
| LET ghost kind attrs(lident_rich) mk_expr(fun_defn)
{ Dlet ($4, ghost $2, $3, apply_partial $2 $5) }
| LET ghost kind attrs(lident_rich) const_defn
{ Dlet ($4, ghost $2, $3, apply_partial $2 $5) }
| LET REC with_list1(rec_defn)
{ Drec $3 }
| EXCEPTION attrs(uident_nq)
{ Dexn ($2, PTtuple [], Ity.MaskVisible) }
| EXCEPTION attrs(uident_nq) return
{ Dexn ($2, fst $3, snd $3) }
ghost:
| (* epsilon *) { false }
| GHOST { true }
| (* epsilon *) { Regular }
| PARTIAL { Partial }
| GHOST { Ghost }
| GHOST PARTIAL
| PARTIAL GHOST { Loc.errorm ~loc:(floc $startpos $endpos)
"Ghost functions cannot be partial" }
kind:
| (* epsilon *) { Expr.RKnone }
......@@ -767,20 +780,15 @@ kind:
| PREDICATE { Expr.RKpred }
| LEMMA { Expr.RKlemma }
%inline partial:
| (* epsilon *) { false }
| PARTIAL { true }
(* Function definitions *)
rec_defn:
| ghost kind partial attrs(lident_rich) binders return_opt spec EQUAL spec seq_expr
{ let pat, ty, mask = $6 in
let spec = apply_return pat (spec_union $7 $9) in
let spec = apply_partial $3 spec in
let id = mk_id return_id $startpos($8) $endpos($8) in
let e = { $10 with expr_desc = Eoptexn (id, mask, $10) } in
$4, $1, $2, $5, ty, mask, spec, e }
| ghost kind attrs(lident_rich) binders return_opt spec EQUAL spec seq_expr
{ let pat, ty, mask = $5 in
let spec = apply_return pat (spec_union $6 $8) in
let id = mk_id return_id $startpos($7) $endpos($7) in
let e = { $9 with expr_desc = Eoptexn (id, mask, $9) } in
$3, ghost $1, $2, $4, ty, mask, apply_partial_sp $1 spec, e }
fun_defn:
| binders return_opt spec EQUAL spec seq_expr
......@@ -893,7 +901,7 @@ single_expr_:
| Pas (p,v,g) -> Pas (push p, v, g)
| Por (p,q) -> Por (push p, q)
| _ -> Pghost pat) in
let pat = if $2 then push $4 else $4 in
let pat = if ghost $2 then push $4 else $4 in
let rec unfold gh d p = match p.pat_desc with
| Pparen p | Pscope (_,p) -> unfold gh d p
| Pghost p -> unfold true d p
......@@ -904,13 +912,13 @@ single_expr_:
| _ when $3 = Expr.RKnone -> Ematch (d, [pat, $8], [])
| _ -> Loc.errorm ~loc:(floc $startpos($3) $endpos($3))
"illegal kind qualifier" in
unfold false $6 pat }
unfold false (apply_partial $2 $6) pat }
| LET ghost kind attrs(lident_op_nq) EQUAL seq_expr IN seq_expr
{ Elet ($4, $2, $3, $6, $8) }
| LET ghost kind partial attrs(lident_nq) mk_expr(fun_defn) IN seq_expr
{ Elet ($5, $2, $3, apply_partial_e $4 $6, $8) }
| LET ghost kind partial attrs(lident_op_nq) mk_expr(fun_defn) IN seq_expr
{ Elet ($5, $2, $3, apply_partial_e $4 $6, $8) }
{ Elet ($4, ghost $2, $3, apply_partial $2 $6, $8) }
| LET ghost kind attrs(lident_nq) mk_expr(fun_defn) IN seq_expr
{ Elet ($4, ghost $2, $3, apply_partial $2 $5, $7) }
| LET ghost kind attrs(lident_op_nq) mk_expr(fun_defn) IN seq_expr
{ Elet ($4, ghost $2, $3, apply_partial $2 $5, $7) }
| LET REC with_list1(rec_defn) IN seq_expr
{ Erec ($3, $5) }
| FUN binders spec ARROW spec seq_expr
......@@ -932,8 +940,8 @@ single_expr_:
let pre = pre_of_any loc ty spec.sp_post in
let spec = { spec with sp_pre = spec.sp_pre @ pre } in
Eany ([], Expr.RKnone, Some ty, mask, spec) }
| VAL ghost kind partial attrs(lident_rich) mk_expr(val_defn) IN seq_expr
{ Elet ($5, $2, $3, apply_partial_e $4 $6, $8) }
| VAL ghost kind attrs(lident_rich) mk_expr(val_defn) IN seq_expr
{ Elet ($4, ghost $2, $3, apply_partial $2 $5, $7) }
| MATCH seq_expr WITH ext_match_cases END
{ let bl, xl = $4 in Ematch ($2, bl, xl) }
| EXCEPTION attrs(uident) IN seq_expr
......@@ -1206,7 +1214,7 @@ pat_uni_:
| pat_arg_ { $1 }
| uqualid pat_arg+ { Papp ($1,$2) }
| GHOST mk_pat(pat_uni_) { Pghost $2 }
| mk_pat(pat_uni_) AS ghost attrs(lident_nq)
| mk_pat(pat_uni_) AS boption(GHOST) attrs(lident_nq)
{ Pas ($1,add_model_trace_attr $4,$3) }
| mk_pat(pat_uni_) cast { Pcast ($1,$2) }
......@@ -1238,7 +1246,7 @@ let_pat_conj_:
let_pat_uni_:
| pat_arg_ { $1 }
| uqualid pat_arg+ { Papp ($1,$2) }
| mk_pat(let_pat_uni_) AS ghost attrs(lident_nq)
| mk_pat(let_pat_uni_) AS boption(GHOST) attrs(lident_nq)
{ Pas ($1,add_model_trace_attr $4,$3) }
| mk_pat(let_pat_uni_) cast { Pcast ($1,$2) }
......
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