Commit 79f564bd authored by Andrei Paskevich's avatar Andrei Paskevich

WhyML: reference variables

caveat: pass-as-reference does not work in chain relations.
        That is, 0 < r += 12 will not typecheck even
        if x is autodereferencing and (+=) has the
        first parameter with the reference marker.

todo: forbid reference markers in logic, in type definitions,
      over logical symbols, etc.

todo: update extraction drivers.
      why3.Ref.Ref defines
        - type "ref",
        - constructor "mk ref" (never used in Typing)
        - projection "contents" (both val and function)
        - program function "ref" (alias for "mk ref")
      ref.Ref defines
        - let-function (!)
        - program function (:=)

      It is important to attribute the symbols to their
      respective modules, since a program with reference
      variables may never use ref.Ref and why3.Ref.Ref
      is imported automatically.
parent 7217aff9
This diff is collapsed.
......@@ -30,13 +30,14 @@ val dity_bool : dity
val dity_unit : dity
type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)
type dref = bool list * bool
(** Patterns *)
type dpattern = private {
dp_pat : pre_pattern;
dp_dity : dity;
dp_vars : dity Mstr.t;
dp_vars : (dity * bool) Mstr.t;
dp_loc : Loc.position option;
}
......@@ -101,7 +102,7 @@ type dexpr = private {
}
and dexpr_node =
| DEvar of string * dvty
| DEvar of string * dvty * dref
| DEsym of prog_symbol
| DEconst of Number.constant * dity
| DEapp of dexpr * dexpr
......@@ -123,7 +124,7 @@ and dexpr_node =
| DEoptexn of preid * dity * mask * dexpr
| DEassert of assertion_kind * term later
| DEpure of term later * dity
| DEvar_pure of string * dvty
| DEvar_pure of string * dvty * dref
| DEls_pure of lsymbol * bool
| DEpv_pure of pvsymbol
| DEabsurd
......@@ -189,6 +190,9 @@ type pre_fun_defn = preid * ghost * rs_kind * dbinder list *
val drec_defn : denv -> pre_fun_defn list -> denv * drec_defn
val undereference : dexpr -> dexpr
(* raises Not_found if the argument is not auto-dereferenced *)
(** Final stage *)
val expr : ?keep_loc:bool -> ?ughost:bool -> dexpr -> expr
......
......@@ -597,7 +597,7 @@ binder:
binder_vars:
| binder_vars_head { fst $1, match snd $1 with
| [] -> Loc.error ~loc:(floc $startpos $endpos) Error
| [] -> Loc.error ~loc:(floc $endpos $endpos) Error
| bl -> List.rev bl }
| binder_vars_rest { $1 }
......@@ -615,15 +615,16 @@ binder_vars_rest:
binder_vars_head:
| ty {
let of_id id = id.id_loc, binder_of_id id in
let push acc = function
| PTtyapp (Qident id, []) -> (id.id_loc, binder_of_id id) :: acc
| _ -> Loc.error ~loc:(floc $startpos $endpos) Error in
| PTtyapp (Qident id, []) -> of_id id :: acc
| _ -> Loc.error ~loc:(floc $endpos $endpos) Error in
match $1 with
| PTtyapp (Qident {id_str = "ref"}, l) ->
true, List.fold_left push [] l
| PTtyapp (Qident id, l) ->
false, List.fold_left push [id.id_loc, binder_of_id id] l
| _ -> Loc.error ~loc:(floc $startpos $endpos) Error }
false, List.fold_left push [of_id id] l
| _ -> Loc.error ~loc:(floc $endpos $endpos) Error }
binder_var:
| attrs(lident_nq) { floc $startpos $endpos, Some $1 }
......@@ -720,6 +721,7 @@ term_dot: mk_term(term_dot_) { $1 }
term_arg_:
| qualid { Tident $1 }
| AMP qualid { Tasref $2 }
| numeral { Tconst $1 }
| TRUE { Ttrue }
| FALSE { Tfalse }
......@@ -881,7 +883,11 @@ assign_expr:
| expr LARROW expr
{ let loc = floc $startpos $endpos in
let rec down ll rl = match ll, rl with
| {expr_desc = Eidapp (q, [e1])}::ll, e2::rl -> (e1,q,e2) :: down ll rl
| ({expr_desc = Eident q} as e1)::ll, e2::rl ->
let e1 = {e1 with expr_desc = Easref q} in
(e1, None, e2) :: down ll rl
| {expr_desc = Eidapp (q, [e1])}::ll, e2::rl ->
(e1, Some q, e2) :: down ll rl
| {expr_desc = Eidapp (Qident id, [_;_]); expr_loc = loc}::_, _::_ ->
begin match Ident.sn_decode id.id_str with
| Ident.SNget _ -> Loc.errorm ~loc
......@@ -1078,6 +1084,7 @@ expr_dot: e = mk_expr(expr_dot_) { e }
expr_arg_:
| qualid { Eident $1 }
| AMP qualid { Easref $2 }
| numeral { Econst $1 }
| TRUE { Etrue }
| FALSE { Efalse }
......
......@@ -74,6 +74,7 @@ and term_desc =
| Tfalse
| Tconst of Number.constant
| Tident of qualid
| Tasref of qualid
| Tidapp of qualid * term list
| Tapply of term * term
| Tinfix of term * ident * term
......@@ -127,6 +128,7 @@ and expr_desc =
| Econst of Number.constant
(* lambda-calculus *)
| Eident of qualid
| Easref of qualid
| Eidapp of qualid * expr list
| Eapply of expr * expr
| Einfix of expr * ident * expr
......@@ -138,7 +140,7 @@ and expr_desc =
| Etuple of expr list
| Erecord of (qualid * expr) list
| Eupdate of expr * (qualid * expr) list
| Eassign of (expr * qualid * expr) list
| Eassign of (expr * qualid option * expr) list
(* control *)
| Esequence of expr * expr
| Eif of expr * expr * expr
......
......@@ -220,6 +220,20 @@ let mk_closure crcmap loc ls =
let vl = Lists.mapi mk_v ls.ls_args in
DTquant (DTlambda, vl, [], mk (DTapp (ls, List.map mk_t vl)))
(* handle auto-dereference in logical terms *)
let vs_dref vs = Sattr.mem Pmodule.ref_attr vs.vs_name.id_attrs
let undereference dt =
let to_deref = function
| DTvar _ -> true (* needed for DEpure *)
| DTgvar vs -> vs_dref vs
| _ -> false in
match dt.dt_node with
| DTapp (ls, [dt])
when ls_equal ls ls_ref_proj && to_deref dt.dt_node -> dt
| _ -> Loc.errorm ?loc:dt.dt_loc "not a reference variable"
(* track the use of labels *)
let at_uses = Hstr.create 5
......@@ -242,7 +256,12 @@ let rec dterm ns km crcmap gvars at denv {term_desc = desc; term_loc = loc} =
Hstr.replace at_uses l true
| None -> ()
end;
func_app (DTgvar v.pv_vs) el
if vs_dref v.pv_vs then
let loc = qloc q and ls = Pmodule.ls_ref_proj in
let e = Dterm.dterm crcmap ~loc (DTgvar v.pv_vs) in
apply_ls loc ls [] ls.ls_args ((loc, e)::el)
else
func_app (DTgvar v.pv_vs) el
| None ->
let ls = find_lsymbol_ns ns q in
apply_ls (qloc q) ls [] ls.ls_args el
......@@ -377,6 +396,10 @@ let rec dterm ns km crcmap gvars at denv {term_desc = desc; term_loc = loc} =
| Ptree.Tscope (q, e1) ->
let ns = import_namespace ns (string_list_of_qualid q) in
DTattr (dterm ns km crcmap gvars at denv e1, Sattr.empty)
| Ptree.Tasref q ->
let e1 = { term_desc = Tident q; term_loc = loc } in
let d1 = dterm ns km crcmap gvars at denv e1 in
DTattr (undereference d1, Sattr.empty)
| Ptree.Tattr (ATpos uloc, e1) ->
DTuloc (dterm ns km crcmap gvars at denv e1, uloc)
| Ptree.Tattr (ATstr attr, e1) ->
......@@ -387,7 +410,6 @@ let rec dterm ns km crcmap gvars at denv {term_desc = desc; term_loc = loc} =
let d1 = dterm ns km crcmap gvars at denv e1 in
DTcast (d1, dty_of_pty ns pty))
let no_gvars at q = match at with
| Some _ -> Loc.errorm ~loc:(qloc q)
"`at' and `old' can only be used in program annotations"
......@@ -410,7 +432,6 @@ let ty_of_pty tuc = ty_of_pty (get_namespace tuc)
let get_namespace muc = List.hd muc.Pmodule.muc_import
let dterm muc =
let uc = muc.muc_theory in
dterm (Theory.get_namespace uc) uc.uc_known uc.uc_crcmap
......@@ -677,8 +698,9 @@ let dbinder muc (_,id,gh,opt) =
let is_reusable de = match de.de_node with
| DEvar _ | DEsym _ -> true | _ -> false
let mk_var n de =
Dexpr.dexpr ?loc:de.de_loc (DEvar (n, de.de_dvty))
let mk_var n { de_dvty = (argl, _ as dvty); de_loc = loc } =
let dref = List.map Util.ffalse argl, false in
Dexpr.dexpr ?loc (DEvar (n, dvty, dref))
let mk_let ~loc n de node =
let de1 = Dexpr.dexpr ~loc node in
......@@ -693,6 +715,10 @@ let local_kind = function
| RKfunc | RKpred -> RKlocal
| k -> k
let undereference ({de_loc = loc} as de) =
try Dexpr.undereference de with Not_found ->
Loc.errorm ?loc "not a reference variable"
let rec eff_dterm muc denv {term_desc = desc; term_loc = loc} =
let expr_app loc e el =
List.fold_left (fun e1 e2 ->
......@@ -721,6 +747,10 @@ let rec eff_dterm muc denv {term_desc = desc; term_loc = loc} =
let muc = open_scope muc "dummy" in
let muc = import_scope muc (string_list_of_qualid q) in
DEattr (eff_dterm muc denv e1, Sattr.empty)
| Ptree.Tasref q ->
let e1 = { term_desc = Tident q; term_loc = loc } in
let d1 = eff_dterm muc denv e1 in
DEattr (undereference d1, Sattr.empty)
| Ptree.Tattr (ATpos uloc, e1) ->
DEuloc (eff_dterm muc denv e1, uloc)
| Ptree.Tattr (ATstr attr, e1) ->
......@@ -924,7 +954,10 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
DEfor (id, efrom, dir, eto, inv, dexpr muc denv e1)
| Ptree.Eassign asl ->
let mk_assign (e1,q,e2) =
dexpr muc denv e1, find_record_field muc q, dexpr muc denv e2 in
let f = match q with
| Some q -> find_record_field muc q
| None -> rs_ref_proj in
dexpr muc denv e1, f, dexpr muc denv e2 in
DEassign (List.map mk_assign asl)
| Ptree.Eraise (q, e1) ->
let xs = find_dxsymbol q in
......@@ -966,6 +999,10 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
let muc = open_scope muc "dummy" in
let muc = import_scope muc (string_list_of_qualid q) in
DEattr (dexpr muc denv e1, Sattr.empty)
| Ptree.Easref q ->
let e1 = { expr_desc = Eident q; expr_loc = loc } in
let d1 = dexpr muc denv e1 in
DEattr (undereference d1, Sattr.empty)
| Ptree.Eattr (ATpos uloc, e1) ->
DEuloc (dexpr muc denv e1, uloc)
| Ptree.Eattr (ATstr attr, e1) ->
......
......@@ -17,7 +17,7 @@ module Ref
let function (!) (r: ref 'a) = r.contents
let (:=) (r:ref 'a) (v:'a) ensures { !r = v } = r.contents <- v
let (:=) (ref r:'a) (v:'a) ensures { r = v } = r <- v
end
......@@ -30,11 +30,11 @@ module Refint
use int.Int
use export Ref
let incr (r: ref int) ensures { !r = old !r + 1 } = r := !r + 1
let decr (r: ref int) ensures { !r = old !r - 1 } = r := !r - 1
let incr (ref r: int) ensures { r = old r + 1 } = r <- r + 1
let decr (ref r: int) ensures { r = old r - 1 } = r <- r - 1
let (+=) (r: ref int) (v: int) ensures { !r = old !r + v } = r := !r + v
let (-=) (r: ref int) (v: int) ensures { !r = old !r - v } = r := !r - v
let ( *= ) (r: ref int) (v: int) ensures { !r = old !r * v } = r := !r * v
let (+=) (ref r: int) (v: int) ensures { r = old r + v } = r <- r + v
let (-=) (ref r: int) (v: int) ensures { r = old r - v } = r <- r - v
let ( *= ) (ref r: int) (v: int) ensures { r = old r * v } = r <- r * v
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