Commit 74afbb53 authored by Andrei Paskevich's avatar Andrei Paskevich

Expr, Dexpr: add checks for top-level let-definitions

parent 6ee91142
......@@ -1153,19 +1153,18 @@ let val_decl ~keep_loc:_ (id,_,_,_,_,_ as vald) =
reunify_regions ();
Loc.try2 ?loc:id.pre_loc val_decl env_empty vald
(* FIXME: unless de is a lambda, no checks are made *)
let let_defn ~keep_loc (id,ghost,kind,de) =
reunify_regions ();
let e = expr ~keep_loc None env_empty false de in
if e.e_ghost && not ghost then Loc.errorm ?loc:id.pre_loc
"Symbol %s must be explicitly marked ghost" id.pre_name;
Loc.try1 ?loc:id.pre_loc (create_let_defn id ~ghost ~kind) e
let rec_defn ~keep_loc drdf =
reunify_regions ();
expr_rec ~keep_loc None env_empty drdf
(* FIXME: unless de is a lambda, no checks are made *)
let expr ~keep_loc de =
reunify_regions ();
expr ~keep_loc None env_empty false de
let e = expr ~keep_loc None env_empty false de in
check_expr e; e
let let_defn ~keep_loc (id,ghost,kind,de) =
let e = expr ~keep_loc de in
if e.e_ghost && not ghost then Loc.errorm ?loc:id.pre_loc
"%s %s must be explicitly marked ghost" (match kind, e.e_vty with
| RKnone, VtyI _ -> "Variable" | _ -> "Function") id.pre_name;
Loc.try1 ?loc:id.pre_loc (create_let_defn id ~ghost ~kind) e
......@@ -747,6 +747,16 @@ let e_fun args p q xq ({e_effect = eff} as e) =
check_expr false mut (cty_r_visible c) Mpv.empty e;
mk_expr (Efun e) (VtyC c) e.e_ghost eff_empty c.cty_reads e.e_syms
let check_expr e = match e.e_node with
| Efun _ -> ()
| _ ->
let e = match e.e_vty with (* rewind if necessary *)
| VtyC c -> e_app_raw e c.cty_args [] c.cty_result
| VtyI _ -> e in
let mut = Spv.fold pv_mut e.e_vars Spv.empty in
let vis = Spv.fold pv_vis e.e_vars Sreg.empty in
check_expr false mut vis Mpv.empty e
(* recursive definitions *)
let rs_clone ({rs_name = id; rs_ghost = ghost} as s) c =
......
......@@ -169,6 +169,12 @@ exception CtyExpected of expr
val ity_of_expr : expr -> ity
val cty_of_expr : expr -> cty
val check_expr : expr -> unit
(** [check_expr e] verifies that [e] does not perform bad
ghost writes nor contains stale (i.e., reset) regions.
This function must be called for any expression which
is used outside of an [Efun]-closure. *)
val e_fold : ('a -> expr -> 'a) -> 'a -> expr -> 'a
val e_find_minimal : (expr -> bool) -> expr -> expr
......
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