Commit 176209a8 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: improve error localisation

parent e74a301d
......@@ -46,8 +46,8 @@ let create_pvsymbol, restore_pv =
let pv = create_pvsymbol id vtv in
Wvs.set vs_to_pv pv.pv_vs pv;
pv),
(fun vs -> try Wvs.find vs_to_pv vs with
Not_found -> raise (Decl.UnboundVar vs))
(fun vs -> try Wvs.find vs_to_pv vs with Not_found ->
Loc.error ?loc:vs.vs_name.id_loc (Decl.UnboundVar vs))
(** program symbols *)
......@@ -146,7 +146,7 @@ let add_pv_vars pv m = Mid.add pv.pv_vs.vs_name pv.pv_vtv.vtv_vars m
let add_vs_vars vs m = add_pv_vars (restore_pv vs) m
let fmla_vars f vsset =
if f.t_ty <> None then raise (FmlaExpected f);
if f.t_ty <> None then Loc.error ?loc:f.t_loc (FmlaExpected f);
Mvs.set_union vsset f.t_vars
let post_vars ity f vsset =
......@@ -527,7 +527,7 @@ let create_let_defn id e =
in
{ let_var = lv ; let_expr = e }
exception StaleRegion of region * ident
exception StaleRegion of expr * region * ident
let check_reset e vars =
(* If we reset a region, then it may only occur in the later code
......@@ -541,7 +541,8 @@ let check_reset e vars =
| Some u when reg_equal u reg -> false
| _ -> ity_v_any Util.ffalse check_reg reg.reg_ity
in
if Sreg.exists check_reg s.vars_reg then raise (StaleRegion (r,id))
if Sreg.exists check_reg s.vars_reg then
Loc.error ?loc:e.e_loc (StaleRegion (e,r,id))
in
Mid.iter check_id vars
in
......@@ -552,7 +553,8 @@ let check_ghost_write e eff =
be read in a later non-ghost code. We ignore any resets:
a once ghostified region must stay so, even if it is reset. *)
let badwr = Sreg.inter e.e_effect.eff_ghostw eff.eff_reads in
if not (Sreg.is_empty badwr) then raise (GhostWrite (e, Sreg.choose badwr))
if not (Sreg.is_empty badwr) then
Loc.error ?loc:e.e_loc (GhostWrite (e, Sreg.choose badwr))
let check_postexpr e eff vars =
check_ghost_write e eff;
......@@ -572,9 +574,8 @@ exception ArrowExpected of expr
let e_app_real e pv =
let vta = match e.e_vty with
| VTarrow vta -> vta
| VTvalue _ -> raise (ArrowExpected e)
in
| VTvalue _ -> Loc.error ?loc:e.e_loc (ArrowExpected e)
| VTarrow vta -> vta in
let eff,vty = vty_app_arrow vta pv.pv_vtv in
check_postexpr e eff (add_pv_vars pv Mid.empty);
let eff = eff_union e.e_effect eff in
......@@ -608,7 +609,7 @@ let on_value fn e = match e.e_node with
| _ ->
let ld = create_let_defn (id_fresh "o") e in
let pv = match ld.let_var with
| LetA _ -> raise (ValueExpected e)
| LetA _ -> Loc.error ?loc:e.e_loc (ValueExpected e)
| LetV pv -> pv in
e_let ld (fn pv)
......@@ -634,7 +635,7 @@ let e_app = List.fold_left (fun e -> on_value (e_app_real e))
let vtv_of_expr e = match e.e_vty with
| VTvalue vtv -> vtv
| VTarrow _ -> raise (ValueExpected e)
| VTarrow _ -> Loc.error ?loc:e.e_loc (ValueExpected e)
let e_plapp pls el ity =
let rec app tl vars ghost eff sbs vtvl argl =
......@@ -730,7 +731,7 @@ let e_assign_real e0 pv =
let vtv0 = vtv_of_expr e0 in
let r = match vtv0.vtv_mut with
| Some r -> r
| None -> raise (Immutable e0) in
| None -> Loc.error ?loc:e0.e_loc (Immutable e0) in
let ghost = vtv0.vtv_ghost || pv.pv_vtv.vtv_ghost in
let eff = eff_assign eff_empty ~ghost r pv.pv_vtv.vtv_ity in
let vars = add_pv_vars pv Mid.empty in
......@@ -752,7 +753,7 @@ let e_assign_real e0 pv =
that every ghost write (whether it was made into a ghost
lvalue or not) is never followed by a non-ghost read. *)
if not vtv0.vtv_ghost && pv.pv_vtv.vtv_ghost then
raise (GhostWrite (e,r));
Loc.error ?loc:e.e_loc (GhostWrite (e,r));
e
let e_assign me e = on_value (e_assign_real me) e
......@@ -787,7 +788,7 @@ let on_fmla fn e = match e.e_node with
| _ ->
let ld = create_let_defn (id_fresh "o") e in
let pv = match ld.let_var with
| LetA _ -> raise (ValueExpected e)
| LetA _ -> Loc.error ?loc:e.e_loc (ValueExpected e)
| LetV pv -> pv in
e_let ld (fn (e_value pv) (t_equ_simp (t_var pv.pv_vs) t_bool_true))
......@@ -888,7 +889,7 @@ let e_try e0 bl =
let remove eff0 (xs,_,_) =
(* we catch in a ghost exception in a non-ghost code *)
if not ghost && Sexn.mem xs eff0.eff_ghostx then
raise (GhostRaise (e0,xs));
Loc.error ?loc:e0.e_loc (GhostRaise (e0,xs));
eff_remove_raise eff0 xs in
let eff0 = List.fold_left remove e0.e_effect bl in
(* total effect and vars *)
......
......@@ -231,7 +231,7 @@ val create_let_defn : preid -> expr -> let_defn
val create_fun_defn : preid -> lambda -> rec_defn
val create_rec_defn : (psymbol * lambda) list -> rec_defn list
exception StaleRegion of region * ident
exception StaleRegion of expr * region * ident
(* freshness violation: a previously reset region is associated to an ident *)
val e_let : let_defn -> expr -> expr
......
......@@ -435,23 +435,43 @@ let print_module fmt m =
let () = Exn_printer.register
begin fun fmt exn -> match exn with
| BadItyArity (ts, ts_arg, app_arg) ->
| Mlw_ty.BadItyArity (ts, ts_arg, app_arg) ->
fprintf fmt "Bad type arity: type symbol %a must be applied \
to %i arguments, but is applied to %i"
print_its ts ts_arg app_arg
| BadRegArity (ts, ts_arg, app_arg) ->
| Mlw_ty.BadRegArity (ts, ts_arg, app_arg) ->
fprintf fmt "Bad region arity: type symbol %a must be applied \
to %i regions, but is applied to %i"
print_its ts ts_arg app_arg
| DuplicateRegion r ->
| Mlw_ty.DuplicateRegion r ->
fprintf fmt "Region %a is used twice" print_reg r
| UnboundRegion r ->
| Mlw_ty.UnboundRegion r ->
fprintf fmt "Unbound region %a" print_reg r
| RegionMismatch (r1,r2) ->
| Mlw_ty.RegionMismatch (r1,r2) ->
fprintf fmt "Region mismatch between %a and %a"
print_regty r1 print_regty r2
| Mlw_ty.TypeMismatch (t1,t2) ->
fprintf fmt "Type mismatch between %a and %a"
print_ity t1 print_ity t2
| Mlw_ty.PolymorphicException (id,_ity) ->
fprintf fmt "Exception %s has a polymorphic type" id.id_string
| Mlw_ty.MutableException (id,_ity) ->
fprintf fmt "The type of exception %s has mutable components" id.id_string
| Mlw_ty.IllegalAlias _reg ->
fprintf fmt "This application creates an illegal alias"
| Mlw_expr.GhostWrite (_e, _reg) ->
fprintf fmt "This expression stores a ghost value in a non-ghost location"
| Mlw_expr.GhostRaise (_e, xs) ->
fprintf fmt "This expression raises a ghost exception %a \
catched by a non-ghost code" print_xs xs
| Mlw_expr.StaleRegion (_e, _reg, id) ->
fprintf fmt "This expression prohibits further \
usage of variable %s" id.id_string
| Mlw_expr.ValueExpected _e ->
fprintf fmt "This expression is not a first-order value"
| Mlw_expr.ArrowExpected _e ->
fprintf fmt "This expression is not a function and cannot be applied"
| Mlw_expr.Immutable _e ->
fprintf fmt "Mutable expression expected"
| _ -> raise exn
end
......@@ -183,6 +183,9 @@ type xsymbol = private {
val xs_equal : xsymbol -> xsymbol -> bool
exception PolymorphicException of ident * ity
exception MutableException of ident * ity
val create_xsymbol : preid -> ity -> xsymbol
module Mexn: Map.S with type key = xsymbol
......@@ -213,6 +216,8 @@ val eff_assign : effect -> ?ghost:bool -> region -> ity -> effect
val eff_remove_raise : effect -> xsymbol -> effect
exception IllegalAlias of region
val eff_full_inst : ity_subst -> effect -> effect
val eff_filter : varset -> effect -> effect
......
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