Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
c61f1bdb
Commit
c61f1bdb
authored
Feb 15, 2017
by
Jean-Christophe Filliâtre
Browse files
renamed Mexn -> Mxs
parent
4ba12926
Changes
12
Hide whitespace changes
Inline
Side-by-side
src/mlw/dexpr.ml
View file @
c61f1bdb
...
...
@@ -375,7 +375,7 @@ type 'a later = pvsymbol Mstr.t -> register_old -> 'a
type
dspec_final
=
{
ds_pre
:
term
list
;
ds_post
:
(
pvsymbol
*
term
)
list
;
ds_xpost
:
(
pvsymbol
*
term
)
list
M
exn
.
t
;
ds_xpost
:
(
pvsymbol
*
term
)
list
M
xs
.
t
;
ds_reads
:
pvsymbol
list
;
ds_writes
:
term
list
;
ds_diverge
:
bool
;
...
...
@@ -775,7 +775,7 @@ let create_invariant pl = List.map to_fmla pl
let
create_post
ity
ql
=
List
.
map
(
fun
(
v
,
f
)
->
ity_equal_check
ity
v
.
pv_ity
;
Ity
.
create_post
v
.
pv_vs
(
to_fmla
f
))
ql
let
create_xpost
xql
=
M
exn
.
mapi
(
fun
xs
ql
->
create_post
xs
.
xs_ity
ql
)
xql
let
create_xpost
xql
=
M
xs
.
mapi
(
fun
xs
ql
->
create_post
xs
.
xs_ity
ql
)
xql
(** User effects *)
...
...
@@ -815,7 +815,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
=
M
exn
.
fold
(
fun
xs
_
eff
->
eff_raise
eff
xs
)
dsp
.
ds_xpost
eff
in
let
eff
=
M
xs
.
fold
(
fun
xs
_
eff
->
eff_raise
eff
xs
)
dsp
.
ds_xpost
eff
in
let
eff
=
if
dsp
.
ds_diverge
then
eff_diverge
eff
else
eff
in
wl
,
eff
...
...
@@ -824,8 +824,8 @@ let effect_of_dspec dsp =
let
check_spec
inr
dsp
ecty
({
e_loc
=
loc
}
as
e
)
=
let
bad_read
reff
eff
=
not
(
Spv
.
subset
reff
.
eff_reads
eff
.
eff_reads
)
in
let
bad_write
weff
eff
=
not
(
Mreg
.
submap
(
fun
_
s1
s2
->
Spv
.
subset
s1
s2
)
weff
.
eff_writes
eff
.
eff_writes
)
in
let
bad_raise
xeff
eff
=
not
(
S
exn
.
subset
xeff
.
eff_raises
eff
.
eff_raises
)
in
weff
.
eff_writes
eff
.
eff_writes
)
in
let
bad_raise
xeff
eff
=
not
(
S
xs
.
subset
xeff
.
eff_raises
eff
.
eff_raises
)
in
(* computed effect vs user effect *)
let
uwrl
,
ue
=
effect_of_dspec
dsp
in
let
ucty
=
create_cty
ecty
.
cty_args
ecty
.
cty_pre
ecty
.
cty_post
...
...
@@ -847,7 +847,7 @@ let check_spec inr dsp ecty ({e_loc = loc} as e) =
"this@ write@ effect@ does@ not@ happen@ in@ the@ expression"
)
uwrl
;
if
check_ue
&&
bad_raise
ueff
eeff
then
Loc
.
errorm
?
loc
"this@ expression@ does@ not@ raise@ exception@ %a"
print_xs
(
S
exn
.
choose
(
S
exn
.
diff
ueff
.
eff_raises
eeff
.
eff_raises
));
print_xs
(
S
xs
.
choose
(
S
xs
.
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"
;
(* check that every computed effect is listed *)
...
...
@@ -858,10 +858,10 @@ let check_spec inr dsp ecty ({e_loc = loc} as e) =
if
check_rw
&&
bad_write
eeff
ueff
then
Loc
.
errorm
?
loc
:
(
e_locate_effect
(
fun
eff
->
bad_write
eff
ueff
)
e
)
"this@ expression@ produces@ an@ unlisted@ write@ effect"
;
if
ecty
.
cty_args
<>
[]
&&
bad_raise
eeff
ueff
then
S
exn
.
iter
(
fun
xs
->
Loc
.
errorm
?
loc
:
(
e_locate_effect
(
fun
eff
->
S
exn
.
mem
xs
eff
.
eff_raises
)
e
)
if
ecty
.
cty_args
<>
[]
&&
bad_raise
eeff
ueff
then
S
xs
.
iter
(
fun
xs
->
Loc
.
errorm
?
loc
:
(
e_locate_effect
(
fun
eff
->
S
xs
.
mem
xs
eff
.
eff_raises
)
e
)
"this@ expression@ raises@ unlisted@ exception@ %a"
print_xs
xs
)
(
S
exn
.
diff
eeff
.
eff_raises
ueff
.
eff_raises
);
print_xs
xs
)
(
S
xs
.
diff
eeff
.
eff_raises
ueff
.
eff_raises
);
if
eeff
.
eff_oneway
&&
not
ueff
.
eff_oneway
then
Loc
.
errorm
?
loc
:
(
e_locate_effect
(
fun
eff
->
eff
.
eff_oneway
)
e
)
"this@ expression@ may@ diverge,@ but@ this@ is@ not@ \
...
...
@@ -1210,8 +1210,8 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
let
vm
,
pat
=
create_prog_pattern
dp
.
dp_pat
xs
.
xs_ity
mask
in
let
e
=
expr
uloc
(
add_pv_map
env
vm
)
de
in
Mstr
.
iter
(
fun
_
v
->
check_used_pv
e
v
)
vm
;
M
exn
.
add
xs
((
pat
,
e
)
::
M
exn
.
find_def
[]
xs
m
)
m
in
let
xsm
=
List
.
fold_left
add_branch
M
exn
.
empty
bl
in
M
xs
.
add
xs
((
pat
,
e
)
::
M
xs
.
find_def
[]
xs
m
)
m
in
let
xsm
=
List
.
fold_left
add_branch
M
xs
.
empty
bl
in
let
is_simple
p
=
match
p
.
pat_node
with
|
Papp
(
fs
,
[]
)
->
is_fs_tuple
fs
|
Pvar
_
|
Pwild
->
true
|
_
->
false
in
...
...
@@ -1259,7 +1259,7 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
let
_
,
pp
=
create_prog_pattern
PPwild
xs
.
xs_ity
mask
in
(
pp
,
e_raise
xs
e
(
ity_of_dity
res
))
::
bl
in
vl
,
e_case
e
(
List
.
rev
bl
)
in
e_try
e1
(
M
exn
.
mapi
mk_branch
xsm
)
e_try
e1
(
M
xs
.
mapi
mk_branch
xsm
)
|
DEraise
(
xs
,
de
)
->
e_raise
xs
(
expr
uloc
env
de
)
(
ity_of_dity
res
)
|
DEghost
de
->
...
...
@@ -1301,7 +1301,7 @@ and rec_defn uloc ({inr = inr} as env) {fds = dfdl} =
let
ghost
=
env
.
ghs
||
gh
||
kind
=
RKlemma
in
let
pvl
=
binders
ghost
bl
in
let
ity
=
Loc
.
try1
?
loc
:
de
.
de_loc
ity_of_dity
(
dity_of_dvty
dvty
)
in
let
cty
=
create_cty
~
mask
pvl
[]
[]
M
exn
.
empty
Mpv
.
empty
eff_empty
ity
in
let
cty
=
create_cty
~
mask
pvl
[]
[]
M
xs
.
empty
Mpv
.
empty
eff_empty
ity
in
let
rs
=
create_rsymbol
id
~
ghost
~
kind
:
RKnone
cty
in
add_rsymbol
env
rs
,
(
rs
,
kind
,
mask
,
dsp
,
dvl
,
de
)
in
let
env
,
fdl
=
Lists
.
map_fold_left
step1
{
env
with
inr
=
true
}
dfdl
in
...
...
@@ -1374,7 +1374,7 @@ let let_defn ?(keep_loc=true) (id, ghost, kind, de) =
let
e
=
expr
uloc
env_empty
de
in
if
mask_ghost
e
.
e_mask
&&
not
ghost
then
Loc
.
errorm
?
loc
"Function %s must be explicitly marked ghost"
nm
;
let
c
=
c_fun
[]
[]
[]
M
exn
.
empty
Mpv
.
empty
e
in
let
c
=
c_fun
[]
[]
[]
M
xs
.
empty
Mpv
.
empty
e
in
(* the rsymbol will carry a single postcondition "the result
is equal to the logical constant". Any user-written spec
will be checked once, in-place, under Eexec. Since kind
...
...
src/mlw/dexpr.mli
View file @
c61f1bdb
...
...
@@ -64,7 +64,7 @@ type 'a later = pvsymbol Mstr.t -> register_old -> 'a
type
dspec_final
=
{
ds_pre
:
term
list
;
ds_post
:
(
pvsymbol
*
term
)
list
;
ds_xpost
:
(
pvsymbol
*
term
)
list
M
exn
.
t
;
ds_xpost
:
(
pvsymbol
*
term
)
list
M
xs
.
t
;
ds_reads
:
pvsymbol
list
;
ds_writes
:
term
list
;
ds_diverge
:
bool
;
...
...
src/mlw/expr.ml
View file @
c61f1bdb
...
...
@@ -171,7 +171,7 @@ let create_projection s v =
let
arg
=
create_pvsymbol
(
id_fresh
"arg"
)
ity
in
let
ls
=
create_fsymbol
id
[
arg
.
pv_vs
.
vs_ty
]
v
.
pv_vs
.
vs_ty
in
let
q
=
make_post
(
fs_app
ls
[
t_var
arg
.
pv_vs
]
v
.
pv_vs
.
vs_ty
)
in
let
c
=
create_cty
[
arg
]
[]
[
q
]
M
exn
.
empty
Mpv
.
empty
eff
v
.
pv_ity
in
let
c
=
create_cty
[
arg
]
[]
[
q
]
M
xs
.
empty
Mpv
.
empty
eff
v
.
pv_ity
in
mk_rs
ls
.
ls_name
c
(
RLls
ls
)
(
Some
v
)
exception
FieldExpected
of
rsymbol
...
...
@@ -198,7 +198,7 @@ let create_constructor ~constr id s fl =
let
eff
=
match
ity
.
ity_node
with
|
Ityreg
r
->
eff_reset
eff_empty
(
Sreg
.
singleton
r
)
|
_
->
eff_empty
in
let
c
=
create_cty
fl
[]
[
q
]
M
exn
.
empty
Mpv
.
empty
eff
ity
in
let
c
=
create_cty
fl
[]
[
q
]
M
xs
.
empty
Mpv
.
empty
eff
ity
in
mk_rs
ls
.
ls_name
c
(
RLls
ls
)
None
let
rs_of_ls
ls
=
...
...
@@ -207,7 +207,7 @@ let rs_of_ls ls =
let
t_args
=
List
.
map
(
fun
v
->
t_var
v
.
pv_vs
)
v_args
in
let
q
=
make_post
(
t_app
ls
t_args
ls
.
ls_value
)
in
let
ity
=
ity_of_ty
(
t_type
q
)
in
let
c
=
create_cty
v_args
[]
[
q
]
M
exn
.
empty
Mpv
.
empty
eff_empty
ity
in
let
c
=
create_cty
v_args
[]
[
q
]
M
xs
.
empty
Mpv
.
empty
eff_empty
ity
in
mk_rs
ls
.
ls_name
c
(
RLls
ls
)
None
(** {2 Program patterns} *)
...
...
@@ -310,7 +310,7 @@ and expr_node =
|
Ecase
of
expr
*
(
prog_pattern
*
expr
)
list
|
Ewhile
of
expr
*
invariant
list
*
variant
list
*
expr
|
Efor
of
pvsymbol
*
for_bounds
*
invariant
list
*
expr
|
Etry
of
expr
*
(
pvsymbol
list
*
expr
)
M
exn
.
t
|
Etry
of
expr
*
(
pvsymbol
list
*
expr
)
M
xs
.
t
|
Eraise
of
xsymbol
*
expr
|
Eassert
of
assertion_kind
*
term
|
Eghost
of
expr
...
...
@@ -375,7 +375,7 @@ let e_fold fn acc e = match e.e_node with
|
Elet
(
LDvar
(
_
,
d
)
,
e
)
|
Ewhile
(
d
,_,_,
e
)
->
fn
(
fn
acc
d
)
e
|
Eif
(
c
,
d
,
e
)
->
fn
(
fn
(
fn
acc
c
)
d
)
e
|
Ecase
(
d
,
bl
)
->
List
.
fold_left
(
fun
acc
(
_
,
e
)
->
fn
acc
e
)
(
fn
acc
d
)
bl
|
Etry
(
d
,
xl
)
->
M
exn
.
fold
(
fun
_
(
_
,
e
)
acc
->
fn
acc
e
)
xl
(
fn
acc
d
)
|
Etry
(
d
,
xl
)
->
M
xs
.
fold
(
fun
_
(
_
,
e
)
acc
->
fn
acc
e
)
xl
(
fn
acc
d
)
exception
FoundExpr
of
Loc
.
position
option
*
expr
...
...
@@ -732,7 +732,7 @@ let c_pur s vl ityl ity =
let
res
=
Opt
.
map
(
fun
_
->
ty_of_ity
ity
)
s
.
ls_value
in
let
q
=
make_post
(
t_app
s
t_args
res
)
in
let
eff
=
eff_ghostify
true
eff_empty
in
let
cty
=
create_cty
v_args
[]
[
q
]
M
exn
.
empty
Mpv
.
empty
eff
ity
in
let
cty
=
create_cty
v_args
[]
[
q
]
M
xs
.
empty
Mpv
.
empty
eff
ity
in
mk_cexp
(
Cpur
(
s
,
vl
))
cty
let
mk_proxy
ghost
e
hd
=
match
e
.
e_node
with
...
...
@@ -806,7 +806,7 @@ let rs_func_app = rs_of_ls fs_func_app
let
ld_func_app
=
let
v_args
=
rs_func_app
.
rs_cty
.
cty_args
in
let
ity
=
rs_func_app
.
rs_cty
.
cty_result
in
let
c
=
create_cty
v_args
[]
[]
M
exn
.
empty
Mpv
.
empty
eff_empty
ity
in
let
c
=
create_cty
v_args
[]
[]
M
xs
.
empty
Mpv
.
empty
eff_empty
ity
in
LDsym
(
rs_func_app
,
c_any
c
)
let
e_func_app
fn
e
=
...
...
@@ -906,19 +906,19 @@ let e_try e xl =
|
[
v
]
->
v
.
pv_ity
,
mask_of_pv
v
|
vl
->
ity_tuple
(
List
.
map
(
fun
v
->
v
.
pv_ity
)
vl
)
,
MaskTuple
(
List
.
map
mask_of_pv
vl
)
in
M
exn
.
iter
(
fun
xs
(
vl
,
d
)
->
M
xs
.
iter
(
fun
xs
(
vl
,
d
)
->
let
ity
,
mask
=
get_mask
vl
in
if
mask_spill
xs
.
xs_mask
mask
then
Loc
.
errorm
"Non-ghost pattern in a ghost position"
;
ity_equal_check
ity
xs
.
xs_ity
;
ity_equal_check
d
.
e_ity
e
.
e_ity
)
xl
;
let
ghost
=
e
.
e_effect
.
eff_ghost
in
let
eeff
=
M
exn
.
fold
(
fun
xs
_
eff
->
let
eeff
=
M
xs
.
fold
(
fun
xs
_
eff
->
eff_catch
eff
xs
)
xl
e
.
e_effect
in
let
dl
=
M
exn
.
fold
(
fun
_
(
_
,
d
)
l
->
d
::
l
)
xl
[]
in
let
dl
=
M
xs
.
fold
(
fun
_
(
_
,
d
)
l
->
d
::
l
)
xl
[]
in
let
add_mask
mask
d
=
mask_union
mask
d
.
e_mask
in
let
mask
=
List
.
fold_left
add_mask
e
.
e_mask
dl
in
let
xeff
=
M
exn
.
fold
(
fun
_
(
vl
,
d
)
eff
->
let
xeff
=
M
xs
.
fold
(
fun
_
(
vl
,
d
)
eff
->
let
add
s
v
=
Spv
.
add_new
(
Invalid_argument
"Expr.e_try"
)
v
s
in
let
deff
=
eff_bind
(
List
.
fold_left
add
Spv
.
empty
vl
)
d
.
e_effect
in
try_effect
dl
eff_union_par
eff
deff
)
xl
eff_empty
in
...
...
@@ -984,7 +984,7 @@ let rec e_rs_subst sm e = e_label_copy e (match e.e_node with
|
Ecase
(
d
,
bl
)
->
e_case
(
e_rs_subst
sm
d
)
(
List
.
map
(
fun
(
pp
,
e
)
->
pp
,
e_rs_subst
sm
e
)
bl
)
|
Etry
(
d
,
xl
)
->
e_try
(
e_rs_subst
sm
d
)
(
M
exn
.
map
(
fun
(
v
,
e
)
->
v
,
e_rs_subst
sm
e
)
xl
))
(
M
xs
.
map
(
fun
(
v
,
e
)
->
v
,
e_rs_subst
sm
e
)
xl
))
and
c_rs_subst
sm
({
c_node
=
n
;
c_cty
=
c
}
as
d
)
=
match
n
with
|
Cany
|
Cpur
_
->
d
...
...
@@ -1311,7 +1311,7 @@ and print_enode pri fmt e = match e.e_node with
|
Eraise
(
xs
,
e
)
->
fprintf
fmt
"raise (%a %a)"
print_xs
xs
print_expr
e
|
Etry
(
e
,
bl
)
->
let
bl
=
M
exn
.
bindings
bl
in
let
bl
=
M
xs
.
bindings
bl
in
fprintf
fmt
"try %a with@
\n
@[<hov>%a@]@
\n
end"
print_expr
e
(
Pp
.
print_list
Pp
.
newline
print_xbranch
)
bl
|
Eabsurd
->
...
...
src/mlw/expr.mli
View file @
c61f1bdb
...
...
@@ -124,7 +124,7 @@ and expr_node = private
|
Ecase
of
expr
*
(
prog_pattern
*
expr
)
list
|
Ewhile
of
expr
*
invariant
list
*
variant
list
*
expr
|
Efor
of
pvsymbol
*
for_bounds
*
invariant
list
*
expr
|
Etry
of
expr
*
(
pvsymbol
list
*
expr
)
M
exn
.
t
|
Etry
of
expr
*
(
pvsymbol
list
*
expr
)
M
xs
.
t
|
Eraise
of
xsymbol
*
expr
|
Eassert
of
assertion_kind
*
term
|
Eghost
of
expr
...
...
@@ -182,7 +182,7 @@ val c_app : rsymbol -> pvsymbol list -> ity list -> ity -> cexp
val
c_pur
:
lsymbol
->
pvsymbol
list
->
ity
list
->
ity
->
cexp
val
c_fun
:
?
mask
:
mask
->
pvsymbol
list
->
pre
list
->
post
list
->
post
list
M
exn
.
t
->
pvsymbol
Mpv
.
t
->
expr
->
cexp
pre
list
->
post
list
->
post
list
M
xs
.
t
->
pvsymbol
Mpv
.
t
->
expr
->
cexp
val
c_any
:
cty
->
cexp
...
...
@@ -218,7 +218,7 @@ val is_e_false : expr -> bool
val
e_raise
:
xsymbol
->
expr
->
ity
->
expr
val
e_try
:
expr
->
(
pvsymbol
list
*
expr
)
M
exn
.
t
->
expr
val
e_try
:
expr
->
(
pvsymbol
list
*
expr
)
M
xs
.
t
->
expr
val
e_case
:
expr
->
(
prog_pattern
*
expr
)
list
->
expr
...
...
src/mlw/ity.ml
View file @
c61f1bdb
...
...
@@ -862,8 +862,8 @@ module Exn = MakeMSH (struct
let
tag
xs
=
Weakhtbl
.
tag_hash
xs
.
xs_name
.
id_tag
end
)
module
S
exn
=
Exn
.
S
module
M
exn
=
Exn
.
M
module
S
xs
=
Exn
.
S
module
M
xs
=
Exn
.
M
(* effects *)
...
...
@@ -883,7 +883,7 @@ type effect = {
eff_taints
:
Sreg
.
t
;
(* ghost code writes *)
eff_covers
:
Sreg
.
t
;
(* surviving writes *)
eff_resets
:
Sreg
.
t
;
(* locked by covers *)
eff_raises
:
S
exn
.
t
;
(* raised exceptions *)
eff_raises
:
S
xs
.
t
;
(* raised exceptions *)
eff_oneway
:
bool
;
(* non-termination *)
eff_ghost
:
bool
;
(* ghost status *)
}
...
...
@@ -894,7 +894,7 @@ let eff_empty = {
eff_taints
=
Sreg
.
empty
;
eff_covers
=
Sreg
.
empty
;
eff_resets
=
Sreg
.
empty
;
eff_raises
=
S
exn
.
empty
;
eff_raises
=
S
xs
.
empty
;
eff_oneway
=
false
;
eff_ghost
=
false
;
}
...
...
@@ -905,13 +905,13 @@ let eff_equal e1 e2 =
Sreg
.
equal
e1
.
eff_taints
e2
.
eff_taints
&&
Sreg
.
equal
e1
.
eff_covers
e2
.
eff_covers
&&
Sreg
.
equal
e1
.
eff_resets
e2
.
eff_resets
&&
S
exn
.
equal
e1
.
eff_raises
e2
.
eff_raises
&&
S
xs
.
equal
e1
.
eff_raises
e2
.
eff_raises
&&
e1
.
eff_oneway
=
e2
.
eff_oneway
&&
e1
.
eff_ghost
=
e2
.
eff_ghost
let
eff_pure
e
=
Mreg
.
is_empty
e
.
eff_writes
&&
S
exn
.
is_empty
e
.
eff_raises
&&
S
xs
.
is_empty
e
.
eff_raises
&&
not
e
.
eff_oneway
let
check_writes
{
eff_writes
=
wrt
}
pvs
=
...
...
@@ -951,7 +951,7 @@ let eff_ghostify gh e =
let
eff_ghostify_weak
gh
e
=
if
not
gh
||
e
.
eff_ghost
then
e
else
if
e
.
eff_oneway
||
not
(
S
exn
.
is_empty
e
.
eff_raises
)
then
e
else
if
e
.
eff_oneway
||
not
(
S
xs
.
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
...
...
@@ -1083,7 +1083,7 @@ let eff_assign asl =
eff_taints
=
taint
;
eff_covers
=
Mreg
.
domain
(
Mreg
.
set_diff
writes
resets
);
eff_resets
=
resets
;
eff_raises
=
S
exn
.
empty
;
eff_raises
=
S
xs
.
empty
;
eff_oneway
=
false
;
eff_ghost
=
ghost
}
in
(* verify that we can rebuild every value *)
...
...
@@ -1108,8 +1108,8 @@ let eff_reset_overwritten ({eff_writes = wr} as e) =
let
svv
,
rst
=
Mreg
.
fold
add_write
wr
(
Sreg
.
empty
,
Sreg
.
empty
)
in
{
e
with
eff_resets
=
Sreg
.
diff
rst
svv
}
let
eff_raise
e
x
=
{
e
with
eff_raises
=
S
exn
.
add
x
e
.
eff_raises
}
let
eff_catch
e
x
=
{
e
with
eff_raises
=
S
exn
.
remove
x
e
.
eff_raises
}
let
eff_raise
e
x
=
{
e
with
eff_raises
=
S
xs
.
add
x
e
.
eff_raises
}
let
eff_catch
e
x
=
{
e
with
eff_raises
=
S
xs
.
remove
x
e
.
eff_raises
}
let
merge_fields
_
f1
f2
=
Some
(
Spv
.
union
f1
f2
)
...
...
@@ -1123,7 +1123,7 @@ let eff_union e1 e2 = {
eff_covers
=
Sreg
.
union
(
remove_stale
e2
e1
.
eff_covers
)
(
remove_stale
e1
e2
.
eff_covers
);
eff_resets
=
Sreg
.
union
e1
.
eff_resets
e2
.
eff_resets
;
eff_raises
=
S
exn
.
union
e1
.
eff_raises
e2
.
eff_raises
;
eff_raises
=
S
xs
.
union
e1
.
eff_raises
e2
.
eff_raises
;
eff_oneway
=
e1
.
eff_oneway
||
e2
.
eff_oneway
;
eff_ghost
=
e1
.
eff_ghost
&&
e2
.
eff_ghost
}
...
...
@@ -1142,12 +1142,12 @@ let eff_union e1 e2 =
let
eff_contaminate
e1
e2
=
if
not
e1
.
eff_ghost
then
e2
else
if
S
exn
.
is_empty
e1
.
eff_raises
then
e2
else
if
S
xs
.
is_empty
e1
.
eff_raises
then
e2
else
eff_ghostify
true
e2
let
eff_contaminate_weak
e1
e2
=
if
not
e1
.
eff_ghost
then
e2
else
if
S
exn
.
is_empty
e1
.
eff_raises
then
eff_ghostify_weak
true
e2
else
if
S
xs
.
is_empty
e1
.
eff_raises
then
eff_ghostify_weak
true
e2
else
eff_ghostify
true
e2
let
eff_union_par
e1
e2
=
...
...
@@ -1221,7 +1221,7 @@ type cty = {
cty_args
:
pvsymbol
list
;
cty_pre
:
pre
list
;
cty_post
:
post
list
;
cty_xpost
:
post
list
M
exn
.
t
;
cty_xpost
:
post
list
M
xs
.
t
;
cty_oldies
:
pvsymbol
Mpv
.
t
;
cty_effect
:
effect
;
cty_result
:
ity
;
...
...
@@ -1256,7 +1256,7 @@ let cty_ghostify gh ({cty_effect = eff} as c) =
let
spec_t_fold
fn_t
acc
pre
post
xpost
=
let
fn_l
a
fl
=
List
.
fold_left
fn_t
a
fl
in
let
acc
=
fn_l
(
fn_l
acc
pre
)
post
in
M
exn
.
fold
(
fun
_
l
a
->
fn_l
a
l
)
xpost
acc
M
xs
.
fold
(
fun
_
l
a
->
fn_l
a
l
)
xpost
acc
let
check_tvs
reads
result
pre
post
xpost
=
(* every type variable in spec comes either from a known vsymbol
...
...
@@ -1284,7 +1284,7 @@ let create_cty ?(mask=MaskVisible) args pre post xpost oldies effect result =
let
exn
=
Invalid_argument
"Ity.create_cty"
in
(* pre, post, and xpost are well-typed *)
check_pre
pre
;
check_post
exn
result
post
;
M
exn
.
iter
(
fun
xs
xq
->
check_post
exn
xs
.
xs_ity
xq
)
xpost
;
M
xs
.
iter
(
fun
xs
xq
->
check_post
exn
xs
.
xs_ity
xq
)
xpost
;
(* mask is consistent with result *)
mask_check
exn
result
mask
;
let
mask
=
mask_reduce
mask
in
...
...
@@ -1295,7 +1295,7 @@ let create_cty ?(mask=MaskVisible) args pre post xpost oldies effect result =
reads are forbidden, to simplify instantiation later. *)
Mpv
.
iter
(
fun
{
pv_ghost
=
gh
;
pv_ity
=
o
}
{
pv_ity
=
t
}
->
if
not
(
gh
&&
o
==
ity_purify
t
)
then
raise
exn
)
oldies
;
let
preads
=
spec_t_fold
t_freepvs
sarg
pre
[]
M
exn
.
empty
in
let
preads
=
spec_t_fold
t_freepvs
sarg
pre
[]
M
xs
.
empty
in
let
qreads
=
spec_t_fold
t_freepvs
Spv
.
empty
[]
post
xpost
in
let
effect
=
eff_read_post
effect
qreads
in
let
oldies
=
Mpv
.
set_inter
oldies
effect
.
eff_reads
in
...
...
@@ -1311,7 +1311,7 @@ let create_cty ?(mask=MaskVisible) args pre post xpost oldies effect result =
|
_
,
{
t_node
=
Tfalse
}
->
true
|
_
->
false
in
let
filter
_
()
=
function
|
[
q
]
when
is_false
q
->
None
|
_
->
Some
()
in
let
raises
=
M
exn
.
diff
filter
effect
.
eff_raises
xpost
in
let
raises
=
M
xs
.
diff
filter
effect
.
eff_raises
xpost
in
let
effect
=
{
effect
with
eff_raises
=
raises
}
in
(* remove effects on unknown regions. We reset eff_taints
instead of simply filtering the existing set in order
...
...
@@ -1388,7 +1388,7 @@ let cty_apply c vl args res =
(
fun
t
->
t_ty_subst
tsb
vsb
t
)
in
let
subst_l
l
=
List
.
map
subst_t
l
in
cty_unsafe
(
List
.
rev
rargs
)
(
subst_l
c
.
cty_pre
)
(
subst_l
c
.
cty_post
)
(
M
exn
.
map
subst_l
c
.
cty_xpost
)
(
subst_l
c
.
cty_post
)
(
M
xs
.
map
subst_l
c
.
cty_xpost
)
oldies
eff
res
c
.
cty_mask
freeze
let
cty_tuple
args
=
...
...
@@ -1401,7 +1401,7 @@ let cty_tuple args =
let
eff
=
eff_read
(
Spv
.
of_list
args
)
in
let
eff
=
eff_ghostify
(
mask
=
MaskGhost
)
eff
in
let
frz
=
List
.
fold_right
freeze_pv
args
isb_empty
in
cty_unsafe
[]
[]
[
post
]
M
exn
.
empty
Mpv
.
empty
eff
res
mask
frz
cty_unsafe
[]
[]
[
post
]
M
xs
.
empty
Mpv
.
empty
eff
res
mask
frz
let
cty_exec_post_raw
c
=
let
ity
=
List
.
fold_right
(
fun
a
ity
->
...
...
@@ -1465,7 +1465,7 @@ let cty_exec ({cty_effect = eff} as c) =
Still, Expr never uses it like this: it is merely attached to Eexec
to provide the converted specification for VC generation. Pvsymbols
that carry the resulting value, however, cannot be generalized. *)
cty_unsafe
[]
pre
post
M
exn
.
empty
Mpv
.
empty
eff
ity
MaskVisible
c
.
cty_freeze
cty_unsafe
[]
pre
post
M
xs
.
empty
Mpv
.
empty
eff
ity
MaskVisible
c
.
cty_freeze
let
cty_exec
c
=
if
c
.
cty_args
=
[]
then
c
else
cty_exec
c
...
...
@@ -1485,14 +1485,14 @@ let cty_read_post c pvs =
let
cty_add_pre
pre
c
=
if
pre
=
[]
then
c
else
begin
check_pre
pre
;
let
c
=
cty_read_pre
(
List
.
fold_left
t_freepvs
Spv
.
empty
pre
)
c
in
let
rd
=
List
.
fold_right
Spv
.
add
c
.
cty_args
c
.
cty_effect
.
eff_reads
in
check_tvs
rd
c
.
cty_result
pre
[]
M
exn
.
empty
;
check_tvs
rd
c
.
cty_result
pre
[]
M
xs
.
empty
;
{
c
with
cty_pre
=
pre
@
c
.
cty_pre
}
end
let
cty_add_post
c
post
=
if
post
=
[]
then
c
else
begin
check_post
(
Invalid_argument
"Ity.cty_add_post"
)
c
.
cty_result
post
;
let
c
=
cty_read_post
c
(
List
.
fold_left
t_freepvs
Spv
.
empty
post
)
in
let
rd
=
List
.
fold_right
Spv
.
add
c
.
cty_args
c
.
cty_effect
.
eff_reads
in
check_tvs
rd
c
.
cty_result
[]
post
M
exn
.
empty
;
check_tvs
rd
c
.
cty_result
[]
post
M
xs
.
empty
;
{
c
with
cty_post
=
post
@
c
.
cty_post
}
end
(** pretty-printing *)
...
...
@@ -1666,7 +1666,7 @@ let print_spec args pre post xpost oldies eff fmt ity =
Pp
.
print_list
Pp
.
nothing
print_pre
fmt
pre
;
Pp
.
print_list
Pp
.
nothing
print_old
fmt
(
Mpv
.
bindings
oldies
);
Pp
.
print_list
Pp
.
nothing
print_post
fmt
post
;
Pp
.
print_list
Pp
.
nothing
print_xpost
fmt
(
M
exn
.
bindings
xpost
)
Pp
.
print_list
Pp
.
nothing
print_xpost
fmt
(
M
xs
.
bindings
xpost
)
let
print_cty
fmt
c
=
print_spec
c
.
cty_args
c
.
cty_pre
c
.
cty_post
c
.
cty_xpost
c
.
cty_oldies
c
.
cty_effect
fmt
(
Some
c
.
cty_result
)
...
...
src/mlw/ity.mli
View file @
c61f1bdb
...
...
@@ -322,8 +322,8 @@ type xsymbol = private {
xs_mask
:
mask
;
}
module
M
exn
:
Extmap
.
S
with
type
key
=
xsymbol
module
S
exn
:
Extset
.
S
with
module
M
=
M
exn
module
M
xs
:
Extmap
.
S
with
type
key
=
xsymbol
module
S
xs
:
Extset
.
S
with
module
M
=
M
xs
val
xs_compare
:
xsymbol
->
xsymbol
->
int
val
xs_equal
:
xsymbol
->
xsymbol
->
bool
...
...
@@ -349,7 +349,7 @@ type effect = private {
eff_taints
:
Sreg
.
t
;
(* ghost code writes *)
eff_covers
:
Sreg
.
t
;
(* surviving writes *)
eff_resets
:
Sreg
.
t
;
(* locked by covers *)
eff_raises
:
S
exn
.
t
;
(* raised exceptions *)
eff_raises
:
S
xs
.
t
;
(* raised exceptions *)
eff_oneway
:
bool
;
(* non-termination *)
eff_ghost
:
bool
;
(* ghost status *)
}
...
...
@@ -402,7 +402,7 @@ type cty = private {
cty_args
:
pvsymbol
list
;
cty_pre
:
pre
list
;
cty_post
:
post
list
;
cty_xpost
:
post
list
M
exn
.
t
;
cty_xpost
:
post
list
M
xs
.
t
;
cty_oldies
:
pvsymbol
Mpv
.
t
;
cty_effect
:
effect
;
cty_result
:
ity
;
...
...
@@ -411,7 +411,7 @@ type cty = private {
}
val
create_cty
:
?
mask
:
mask
->
pvsymbol
list
->
pre
list
->
post
list
->
post
list
M
exn
.
t
->
pre
list
->
post
list
->
post
list
M
xs
.
t
->
pvsymbol
Mpv
.
t
->
effect
->
ity
->
cty
(** [create_cty ?mask args pre post xpost oldies effect result] creates
a computation type. [post] and [mask] must be consistent with [result].
...
...
@@ -496,5 +496,5 @@ val print_pvty : Format.formatter -> pvsymbol -> unit (* pvsymbol : type *)
val
print_cty
:
Format
.
formatter
->
cty
->
unit
(* computation type *)
val
print_spec
:
pvsymbol
list
->
pre
list
->
post
list
->
post
list
M
exn
.
t
->
pvsymbol
Mpv
.
t
pvsymbol
list
->
pre
list
->
post
list
->
post
list
M
xs
.
t
->
pvsymbol
Mpv
.
t
->
effect
->
Format
.
formatter
->
ity
option
->
unit
(* piecemeal cty *)
src/mlw/pdecl.ml
View file @
c61f1bdb
...
...
@@ -65,7 +65,7 @@ let create_semi_constructor id s fdl pjl invl =
let
eff
=
match
ity
.
ity_node
with
|
Ityreg
r
->
eff_reset
eff_empty
(
Sreg
.
singleton
r
)
|
_
->
eff_empty
in
let
c
=
create_cty
fdl
invl
[
q
]
M
exn
.
empty
Mpv
.
empty
eff
ity
in
let
c
=
create_cty
fdl
invl
[
q
]
M
xs
.
empty
Mpv
.
empty
eff
ity
in
create_rsymbol
id
c
let
create_plain_record_decl
~
priv
~
mut
id
args
fdl
invl
=
...
...
@@ -186,8 +186,8 @@ let get_syms node pure =
let
add_tl
syms
tl
=
syms_tl
syms
tl
in
let
add_xq
xs
ql
syms
=
syms_xs
xs
(
add_tl
syms
ql
)
in
let
syms
=
add_tl
(
add_tl
syms
c
.
cty_pre
)
c
.
cty_post
in
let
syms
=
M
exn
.
fold
add_xq
c
.
cty_xpost
syms
in
S
exn
.
fold
syms_xs
c
.
cty_effect
.
eff_raises
syms
in
let
syms
=
M
xs
.
fold
add_xq
c
.
cty_xpost
syms
in
S
xs
.
fold
syms_xs
c
.
cty_effect
.
eff_raises
syms
in
let
rec
syms_expr
syms
e
=
match
e
.
e_node
with
|
Evar
_
|
Econst
_
|
Eabsurd
->
syms
|
Eassert
(
_
,
t
)
|
Epure
t
->
syms_term
syms
t
...
...
@@ -226,7 +226,7 @@ let get_syms node pure =
|
Etry
(
d
,
xl
)
->
let
add_branch
xs
(
vl
,
e
)
syms
=
syms_xs
xs
(
syms_pvl
(
syms_expr
syms
e
)
vl
)
in
M
exn
.
fold
add_branch
xl
(
syms_expr
syms
d
)
M
xs
.
fold
add_branch
xl
(
syms_expr
syms
d
)
|
Eraise
(
xs
,
e
)
->
syms_xs
xs
(
syms_eity
syms
e
)
and
syms_eity
syms
e
=
...
...
src/mlw/pinterp.ml
View file @
c61f1bdb
...
...
@@ -623,7 +623,7 @@ let rec eval_expr env (e : expr) : result =
match
r
with
|
Excep
(
ex
,
t
)
->
begin
match
M
exn
.
find
ex
el
with
match
M
xs
.
find
ex
el
with
|
([]
,
e2
)
->
(* assert (t = Vvoid); *)
eval_expr
env
e2
...
...
src/mlw/pmodule.ml
View file @
c61f1bdb
...
...
@@ -116,7 +116,7 @@ and mod_inst = {
mi_pk
:
prop_kind
Mpr
.
t
;
mi_pv
:
pvsymbol
Mvs
.
t
;
mi_rs
:
rsymbol
Mrs
.
t
;
mi_xs
:
xsymbol
M
exn
.
t
;
mi_xs
:
xsymbol
M
xs
.
t
;
}
let
empty_mod_inst
m
=
{
...
...
@@ -128,7 +128,7 @@ let empty_mod_inst m = {
mi_pk
=
Mpr
.
empty
;
mi_pv
=
Mvs
.
empty
;
mi_rs
=
Mrs
.
empty
;
mi_xs
=
M
exn
.
empty
;
mi_xs
=
M
xs
.
empty
;
}
(** {2 Module under construction} *)
...
...
@@ -364,7 +364,7 @@ type clones = {
mutable
fd_table
:
pvsymbol
Mpv
.
t
;
mutable
pv_table
:
pvsymbol
Mvs
.
t
;
mutable
rs_table
:
rsymbol
Mrs
.
t
;
mutable
xs_table
:
xsymbol
M
exn
.
t
;
mutable
xs_table
:
xsymbol
M
xs
.
t
;
}
let
empty_clones
m
=
{
...
...
@@ -377,7 +377,7 @@ let empty_clones m = {
fd_table
=
Mpv
.
empty
;
pv_table
=
Mvs
.
empty
;
rs_table
=
Mrs
.
empty
;
xs_table
=
M
exn
.
empty
;
xs_table
=
M
xs
.
empty
;
}
(* populate the clone structure *)
...
...
@@ -468,7 +468,7 @@ let cl_find_rs cl rs =
let
cl_find_xs
cl
xs
=
if
not
(
Sid
.
mem
xs
.
xs_name
cl
.
cl_local
)
then
xs
else
M
exn
.
find
xs
cl
.
xs_table
else
M
xs
.
find
xs
cl
.
xs_table
let
clone_ls
inst
cl
ls
=
if
Mls
.
mem
ls
inst
.
mi_ls
then
raise
(
CannotInstantiate
ls
.
ls_name
);
...
...
@@ -526,7 +526,7 @@ let cl_init_xs cl ({xs_name = id} as xs) xs' =
with
TypeMismatch
_
->
raise
(
BadInstance
id
)
end
;
if
mask_spill
xs'
.
xs_mask
xs
.
xs_mask
then
raise
(
BadInstance
id
);
cl
.
xs_table
<-
M
exn
.
add
xs
xs'
cl
.
xs_table
cl
.
xs_table
<-
M
xs
.
add
xs
xs'
cl
.
xs_table
let
cl_init_pv
cl
({
vs_name
=
id
}
as
vs
)
pv'
=
let
pv
=
restore_pv
vs
in
...
...
@@ -546,7 +546,7 @@ let cl_init m inst =
Mls
.
iter
(
cl_init_ls
cl
)
inst
.
mi_ls
;
Mrs
.
iter
(
cl_init_rs
cl
)
inst
.
mi_rs
;
Mvs
.
iter
(
cl_init_pv
cl
)
inst
.
mi_pv
;
M
exn
.
iter
(
cl_init_xs
cl
)
inst
.
mi_xs
;
M
xs
.
iter
(
cl_init_xs
cl
)
inst
.
mi_xs
;
Mpr
.
iter
(
cl_init_pr
cl
)
inst
.
mi_pk
;
cl
...
...
@@ -744,10 +744,10 @@ let clone_cty cl sm ?(drop_decr=false) cty =
let
pre
=
if
drop_decr
then
List
.
tl
cty
.
cty_pre
else
cty
.
cty_pre
in
let
pre
=
clone_invl
cl
sm_args
pre
in
let
post
=
clone_invl
cl
sm_olds
cty
.
cty_post
in
let
xpost
=
M
exn
.
fold
(
fun
xs
fl
q
->
let
xpost
=
M
xs
.
fold
(
fun
xs
fl
q
->
let
xs
=
cl_find_xs
cl
xs
in
let
fl
=
clone_invl
cl
sm_olds
fl
in
M
exn
.
add
xs
fl
q
)
cty
.
cty_xpost
M
exn
.
empty
in
M
xs
.
add
xs
fl
q
)
cty
.
cty_xpost
M
xs
.
empty
in
let
add_read
v
s
=
Spv
.
add
(
sm_find_pv
sm_args
v
)
s
in
let
reads
=
Spv
.
fold
add_read
(
cty_reads
cty
)
Spv
.
empty
in
let
reads
=
List
.
fold_right
add_read
cty
.
cty_args
reads
in
...
...
@@ -760,7 +760,7 @@ let clone_cty cl sm ?(drop_decr=false) cty =
let
resets
=
Sreg
.
fold
add_reset
cty
.
cty_effect
.
eff_resets
Sreg
.
empty
in
let
eff
=
eff_reset
(
eff_write
reads
writes
)
resets
in
let
add_raise
xs
eff
=
eff_raise
eff
(
cl_find_xs
cl
xs
)
in
let
eff
=
S
exn
.
fold
add_raise
cty
.
cty_effect
.
eff_raises
eff
in
let
eff
=
S
xs
.
fold
add_raise
cty
.
cty_effect
.
eff_raises
eff
in
let
eff
=
if
cty
.
cty_effect
.
eff_oneway
then
eff_diverge
eff
else
eff
in
let
cty
=
create_cty
~
mask
:
cty
.
cty_mask
args
pre
post
xpost
olds
eff
res
in
cty_ghostify
(
cty_ghost
cty
)
cty
...
...
@@ -826,8 +826,8 @@ let rec clone_expr cl sm e = e_label_copy e (match e.e_node with
let
conv_br
xs
(
vl
,
e
)
m
=
let
vl'
=
List
.
map
(
clone_pv
cl
)
vl
in
let
sm
=
List
.
fold_left2
sm_save_pv
sm
vl
vl'
in
M
exn
.
add
(
cl_find_xs
cl
xs
)
(
vl'
,
clone_expr
cl
sm
e
)
m
in
e_try
(
clone_expr
cl
sm
d
)
(
M
exn
.
fold
conv_br
xl
M
exn
.
empty
)
M
xs
.
add
(
cl_find_xs
cl
xs
)
(
vl'
,
clone_expr
cl
sm
e
)
m
in
e_try
(
clone_expr
cl
sm
d
)
(
M
xs
.
fold
conv_br
xl
M
xs
.
empty
)
|
Eraise
(
xs
,
e
)
->
e_raise
(
cl_find_xs
cl
xs
)
(
clone_expr
cl
sm
e
)
(
clone_ity
cl
e
.
e_ity
)