Commit 17ed1270 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

Add support for partial functions

Program functions can be declared as partial with "let/val partial".
Similarly to "diverges", partial code cannot be ghost, however it does not need to be
explicitly specified as partial.

Fixes #184.
parent 8e5da6fb
val function partial f (x:int) : unit
\ No newline at end of file
val ghost partial f () : int
\ No newline at end of file
val partial random () : int
let ghost f () = random ()
val partial random () : int
let ghost f () = random ()
\ No newline at end of file
val partial f (x:int) : unit
let main () =
let ghost s = 3 in
f s;
42
\ No newline at end of file
let lemma partial f (x:int)
ensures { true }
= ()
\ No newline at end of file
let partial f () = 2
\ No newline at end of file
val partial random () : int
type t = { x: int } invariant { x = 0 } by { x = random () }
\ No newline at end of file
val partial random () : int
val f (x:int) : unit
use int.Int
let main () =
let r = random () in
let s = random () in
let ghost x = random () in
f x;
f r;
f x;
r * s
\ No newline at end of file
......@@ -120,6 +120,7 @@ let d2 : Ptree.decl =
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let body: expr = mk_expr Etrue in
......@@ -150,6 +151,7 @@ let d3 : Ptree.decl =
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let body: expr = mk_evar id_b in
......@@ -184,6 +186,7 @@ let d1 : Ptree.decl =
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let body: expr = mk_expr (Ecast (mk_econst "42", PTtyapp (Qident a, []))) in
......
......@@ -117,6 +117,7 @@ let d1 : decl =
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let body = mk_eapp mul_int [mk_evar id_x; mk_econst "7"] in
......@@ -163,6 +164,7 @@ let d2 =
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let body =
......@@ -221,6 +223,7 @@ let d3 =
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let body =
......
......@@ -79,6 +79,7 @@ let empty_spec = {
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
type env = {
......
......@@ -38,7 +38,7 @@
sp_pre = []; sp_post = []; sp_xpost = [];
sp_reads = []; sp_writes = []; sp_alias = [];
sp_variant = [];
sp_checkrw = false; sp_diverge = false;
sp_checkrw = false; sp_diverge = false; sp_partial = false;
}
let spec_union s1 s2 = {
......@@ -51,6 +51,7 @@
sp_variant = variant_union s1.sp_variant s2.sp_variant;
sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
sp_diverge = s1.sp_diverge || s2.sp_diverge;
sp_partial = s1.sp_partial || s2.sp_partial;
}
%}
......
......@@ -25,7 +25,7 @@
(defconst why3-font-lock-keywords-1
(list
`(,(why3-regexp-opt '("invariant" "variant" "diverges" "requires" "ensures" "pure" "returns" "raises" "reads" "writes" "alias" "assert" "assume" "check")) . font-lock-type-face)
`(,(why3-regexp-opt '("use" "clone" "scope" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "raise" "return" "break" "continue" "try" "with" "theory" "uses" "module" "converter" "fun" "at" "old" "true" "false" "forall" "exists" "label" "by" "so" "meta")) . font-lock-keyword-face)
`(,(why3-regexp-opt '("use" "clone" "scope" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "partial" "raise" "return" "break" "continue" "try" "with" "theory" "uses" "module" "converter" "fun" "at" "old" "true" "false" "forall" "exists" "label" "by" "so" "meta")) . font-lock-keyword-face)
)
"Minimal highlighting for Why3 mode")
......
......@@ -93,7 +93,7 @@ syn keyword whyKeyword then type with
syn keyword whyKeyword abstract any break continue
syn keyword whyKeyword exception fun ghost label
syn keyword whyKeyword model mutable private
syn keyword whyKeyword model mutable partial private
syn keyword whyKeyword raise rec return val while
syn keyword whyBoolean true false
......
......@@ -384,6 +384,7 @@ type dspec_final = {
ds_reads : pvsymbol list;
ds_writes : term list;
ds_diverge : bool;
ds_partial : bool;
ds_checkrw : bool;
}
......@@ -892,6 +893,7 @@ let effect_of_dspec dsp =
Loc.errorm ?loc:t.t_loc "mutable expression expected" in
let wl, eff = List.fold_left add_write ([], eff_read pvs) dsp.ds_writes in
let eff = Mxs.fold (fun xs _ eff -> eff_raise eff xs) dsp.ds_xpost eff in
let eff = if dsp.ds_partial then eff_partial eff else eff in
let eff = if dsp.ds_diverge then eff_diverge eff else eff in
wl, eff
......@@ -924,8 +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 && ueff.eff_oneway && not eeff.eff_oneway then Loc.errorm ?loc
"this@ expression@ does@ not@ diverge";
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";
(* check that every computed effect is listed *)
if check_rw && bad_read eeff ueff then Loc.errorm ?loc
"this@ expression@ depends@ on@ variable@ %a,@ \
......
......@@ -76,6 +76,7 @@ type dspec_final = {
ds_reads : pvsymbol list;
ds_writes : term list;
ds_diverge : bool;
ds_partial : bool;
ds_checkrw : bool;
}
......
......@@ -74,8 +74,10 @@ let rs_kind s = match s.rs_logic with
let rs_ghost s = s.rs_cty.cty_effect.eff_ghost
let check_effects ?loc c =
if c.cty_effect.eff_oneway then Loc.errorm ?loc
if diverges c.cty_effect.eff_oneway then Loc.errorm ?loc
"This function may not terminate, it cannot be used as pure";
if partial c.cty_effect.eff_oneway then Loc.errorm ?loc
"This function may fail, it cannot be used as pure";
if not (cty_pure c) then Loc.errorm ?loc
"This function has side effects, it cannot be used as pure"
......@@ -451,7 +453,7 @@ let localize_reset_stale v r el =
(* localize a divergence *)
let localize_divergence el =
let diverges eff = eff.eff_oneway in
let diverges eff = diverges eff.eff_oneway in
List.iter (fun e -> if diverges e.e_effect then
let loc = e_locate_effect diverges e in
Loc.error ?loc GhostDivergence) el;
......@@ -1149,7 +1151,7 @@ let ls_decr_of_rec_defn = function
| { rec_rsym = {rs_cty = {cty_pre = {t_node = Tapp (ls,_)}::_}} } -> Some ls
| _ -> None
(* pretty-pringting *)
(* pretty-printing *)
open Format
open Pretty
......@@ -1172,7 +1174,7 @@ let forget_let_defn = function
let print_rs fmt s =
Ident.print_decoded fmt (id_unique sprinter (id_of_rs s))
let print_rs_head fmt s = fprintf fmt "%s%s%a%a"
let print_rs_head fmt s = fprintf fmt "%s%s%s%a%a"
(if s.rs_cty.cty_effect.eff_ghost then "ghost " else "")
(match s.rs_logic with
| RLnone -> ""
......@@ -1180,6 +1182,7 @@ let print_rs_head fmt s = fprintf fmt "%s%s%a%a"
| 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 =
......
......@@ -868,16 +868,30 @@ exception IllegalAssign of region * region * region
exception ImpureVariable of tvsymbol * ity
exception GhostDivergence
type termination_status =
| Ghostifiable
| Partial
| Diverges
let ghostifiable status = (status = Ghostifiable)
let partial status = (status = Partial)
let diverges status = (status = Diverges)
let termination_union t1 t2 = match (t1, t2) with
| Ghostifiable, Ghostifiable -> Ghostifiable
| _, 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 : bool; (* 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 : termination_status; (* non-termination *)
eff_ghost : bool; (* ghost status *)
}
let eff_empty = {
......@@ -888,7 +902,7 @@ let eff_empty = {
eff_resets = Sreg.empty;
eff_raises = Sxs.empty;
eff_spoils = Stv.empty;
eff_oneway = false;
eff_oneway = Ghostifiable;
eff_ghost = false;
}
......@@ -906,7 +920,7 @@ let eff_equal e1 e2 =
let eff_pure e =
Mreg.is_empty e.eff_writes &&
Sxs.is_empty e.eff_raises &&
not e.eff_oneway
ghostifiable e.eff_oneway
let check_writes {eff_writes = wrt} pvs =
if not (Mreg.is_empty wrt) then Spv.iter (fun v ->
......@@ -940,12 +954,12 @@ let reset_taints e =
let eff_ghostify gh e =
if not gh || e.eff_ghost then e else
if e.eff_oneway then raise GhostDivergence else
if (not (ghostifiable 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 e.eff_oneway || not (Sxs.is_empty e.eff_raises) then e else
if not (ghostifiable 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
......@@ -953,9 +967,14 @@ let eff_ghostify_weak gh e =
Therefore, we check that all visible writes are already taints. *)
eff_ghostify gh e
let eff_diverge e = if e.eff_oneway then e else
let eff_partial e =
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
if e.eff_ghost then raise GhostDivergence else
{ e with eff_oneway = true }
{ e with eff_oneway = Diverges }
let eff_read_pre rd e =
if Spv.subset rd e.eff_reads then e else
......@@ -1077,7 +1096,7 @@ let eff_assign asl =
eff_resets = resets;
eff_raises = Sxs.empty;
eff_spoils = Stv.empty;
eff_oneway = false;
eff_oneway = Ghostifiable;
eff_ghost = ghost } in
(* verify that we can rebuild every value *)
check_writes effect reads;
......@@ -1120,7 +1139,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 = e1.eff_oneway || e2.eff_oneway;
eff_oneway = termination_union e1.eff_oneway e2.eff_oneway;
eff_ghost = e1.eff_ghost && e2.eff_ghost }
let eff_union e1 e2 =
......@@ -1481,8 +1500,10 @@ 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 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
"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";
if not (Mreg.is_empty c.cty_freeze.isb_reg) then Loc.errorm
......@@ -1679,7 +1700,7 @@ let print_spec args pre post xpost oldies eff fmt ity =
fprintf fmt "@[<hov 4>@[%a@]%a@]"
(Pp.print_list_pre Pp.space print_pvty) args
(Pp.print_option print_result) ity;
if eff.eff_oneway then pp_print_string fmt " diverges";
if diverges eff.eff_oneway then pp_print_string fmt " diverges";
let reads = List.fold_right Spv.remove args eff.eff_reads in
if not (Spv.is_empty reads) then fprintf fmt "@\nreads { @[%a@] }"
(Pp.print_list Pp.comma print_pv) (Spv.elements reads);
......
......@@ -339,16 +339,25 @@ exception IllegalAssign of region * region * region
exception ImpureVariable of tvsymbol * ity
exception GhostDivergence
type termination_status =
| Ghostifiable
| Partial
| Diverges
val ghostifiable : termination_status -> bool
val partial : termination_status -> bool
val diverges : termination_status -> 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 : bool; (* 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 : termination_status; (* non-termination *)
eff_ghost : bool; (* ghost status *)
}
val eff_empty : effect
......@@ -377,9 +386,10 @@ val eff_catch : effect -> xsymbol -> effect
val eff_spoil : effect -> ity -> effect
val eff_diverge : effect -> effect (* forbidden if ghost *)
val eff_ghostify : bool -> effect -> effect (* forbidden if diverges *)
val eff_ghostify_weak : bool -> effect -> effect (* only if has no effect *)
val eff_partial : effect -> effect (* forbidden if ghost *)
val eff_diverge : effect -> effect (* forbidden if ghost *)
val eff_ghostify : bool -> effect -> effect (* forbidden if fails or diverges *)
val eff_ghostify_weak : bool -> effect -> effect (* only if has no effect *)
val eff_union_seq : effect -> effect -> effect (* checks for stale variables *)
val eff_union_par : effect -> effect -> effect (* no stale-variable check *)
......
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