Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
852ed2a9
Commit
852ed2a9
authored
May 28, 2011
by
Jean-Christophe Filliâtre
Browse files
programs: mutable field assignment
parent
d2fad71d
Changes
18
Hide whitespace changes
Inline
Side-by-side
bench/programs/bad-typing/alias1.mlw
View file @
852ed2a9
module M
use import module
stdlib
.Ref
use import module
ref
.Ref
let foo (x : ref int) (y : ref int) =
x := 1;
...
...
bench/programs/bad-typing/alias2.mlw
View file @
852ed2a9
module M
use import module
stdlib
.Ref
use import module
ref
.Ref
let foo (x : ref int) (y : ref int) =
x := 1;
...
...
bench/programs/bad-typing/alias3.mlw
View file @
852ed2a9
module M
use import module
stdlib
.Ref
use import module
ref
.Ref
let foo (x : ref int) (y : ref int) =
x := 1;
...
...
bench/programs/bad-typing/effect1.mlw
View file @
852ed2a9
module M
use import module
stdlib
.Ref
use import module
ref
.Ref
parameter f : x:int -> {} unit writes a.contents {}
...
...
bench/programs/bad-typing/effect2.mlw
View file @
852ed2a9
module M
use import module
stdlib
.Ref
use import module
ref
.Ref
parameter f : x:int -> {} unit writes x.contents {}
...
...
bench/programs/bad-typing/effect3.mlw
View file @
852ed2a9
module M
use import module
stdlib
.Ref
use import module
ref
.Ref
parameter a : int
...
...
bench/programs/bad-typing/effect4.mlw
View file @
852ed2a9
module M
use import module
stdlib
.Ref
use import module
ref
.Ref
parameter foo : int -> int
...
...
bench/programs/bad-typing/fresh1.mlw
View file @
852ed2a9
module P
use import module
stdlib
.Ref
use import module
ref
.Ref
let f (a : ref int) =
a
let f (a : ref int) =
todo (* TODO *)
end
modules/ref.mlw
View file @
852ed2a9
...
...
@@ -6,11 +6,14 @@ module Ref
logic (!) (x: ref 'a) : 'a = x.contents
parameter ref : v:'a -> {} ref 'a { result = {| contents = v |} }
(* parameter ref : v:'a -> {} ref 'a { result = {| contents = v |} } *)
let ref (v: 'a) = {} {| contents = v |} { result = {| contents = v |} }
parameter (!) : r:ref 'a -> {} 'a reads r { result = !r }
(* parameter (!) : r:ref 'a -> {} 'a reads r { result = !r } *)
let (!) (r:ref 'a) = {} r.contents { result = !r }
parameter (:=) : r:ref 'a -> v:'a -> {} unit writes r { !r = v }
(* parameter (:=) : r:ref 'a -> v:'a -> {} unit writes r { !r = v } *)
let (:=) (r:ref 'a) (v:'a) = {} r.contents <- v { !r = v }
end
...
...
@@ -24,3 +27,9 @@ module Refint
parameter decr : r:ref int -> {} unit writes r { !r = old !r - 1 }
end
(*
Local Variables:
compile-command: "unset LANG; make -C .. modules/ref"
End:
*)
src/parser/parser.pre.mly
View file @
852ed2a9
...
...
@@ -1030,11 +1030,11 @@ expr:
mk_expr
(
mk_apply_id
{
id
=
"notb"
;
id_lab
=
[]
;
id_loc
=
floc
()
}
[
t
])
}
|
expr
LARROW
expr
{
match
$
1
.
expr_desc
with
|
Ea
pply
(
e1
1
,
e12
)
->
begin
match
e11
.
expr_desc
with
|
Eident
x
->
mk_expr
(
Eassign
(
e12
,
x
,
$
3
))
|
Ea
ccess
(
e1
,
x
)
->
mk_expr
(
Eassign
(
e1
,
x
,
$
3
))
|
Eapply
(
e11
,
e12
)
->
begin
match
e11
.
expr_desc
with
|
Eapply
({
expr_desc
=
Eident
(
Qident
x
)
}
,
e11
)
when
x
.
id
=
mixfix
"[]"
->
when
x
.
id
=
mixfix
"[]"
->
mk_mixfix3
"[]<-"
e11
e12
$
3
|
_
->
raise
Parsing
.
Parse_error
...
...
@@ -1132,7 +1132,7 @@ expr_dot:
expr_sub
:
|
expr_dot
DOT
lqualid_rich
{
mk_expr
(
mk_apply
(
mk_expr_i
3
(
Eident
$
3
))
[
$
1
]
)
}
{
mk_expr
(
Eaccess
(
$
1
,
$
3
)
)
}
|
LEFTPAR
expr
RIGHTPAR
{
$
2
}
|
BEGIN
expr
END
...
...
src/parser/ptree.ml
View file @
852ed2a9
...
...
@@ -211,6 +211,7 @@ and expr_desc =
|
Eletrec
of
(
ident
*
binder
list
*
variant
option
*
triple
)
list
*
expr
|
Etuple
of
expr
list
|
Erecord
of
(
qualid
*
expr
)
list
|
Eaccess
of
expr
*
qualid
|
Eassign
of
expr
*
qualid
*
expr
(* control *)
|
Esequence
of
expr
*
expr
...
...
src/programs/TODO
View file @
852ed2a9
o
pas de old dans les invariant
s
o
freshness analysi
s
o
e <- e
o
no `old' in loop invariants
o {| e with x1 = e1; ...; xn = en |}
o WP: update
o syntactic sugar for postcondition:
{ pat | q } stands for { let pat = result in q }
...
...
@@ -36,4 +34,4 @@ o library
- List
- Map
- Set
\ No newline at end of file
- Set
src/programs/pgm_pretty.ml
View file @
852ed2a9
...
...
@@ -76,7 +76,7 @@ let rec print_expr fmt e = match e.expr_desc with
fprintf
fmt
"absurd"
and
print_pv
fmt
v
=
fprintf
fmt
"<@[%a
: %a
@]>"
print_vs
v
.
pv_effect
print_ty
v
.
pv_pure
.
vs_ty
fprintf
fmt
"<@[%a@]>"
print_vs
ty
v
.
pv_effect
and
print_triple
fmt
(
p
,
e
,
q
)
=
fprintf
fmt
"@[<hv 0>%a@ %a@ %a@]"
print_pre
p
print_expr
e
print_post
q
...
...
src/programs/pgm_ttree.ml
View file @
852ed2a9
...
...
@@ -111,6 +111,8 @@ and dexpr_desc =
|
DEfun
of
dubinder
list
*
dtriple
|
DElet
of
ident
*
dexpr
*
dexpr
|
DEletrec
of
drecfun
list
*
dexpr
|
DEaccess
of
dexpr
*
Term
.
lsymbol
*
int
option
|
DEassign
of
dexpr
*
Term
.
lsymbol
*
int
*
dexpr
|
DEsequence
of
dexpr
*
dexpr
|
DEif
of
dexpr
*
dexpr
*
dexpr
...
...
@@ -204,6 +206,7 @@ and iexpr_desc =
|
IEfun
of
ibinder
list
*
itriple
|
IElet
of
ivsymbol
*
iexpr
*
iexpr
|
IEletrec
of
irecfun
list
*
iexpr
|
IEaccess
of
ivsymbol
*
Term
.
lsymbol
*
R
.
t
option
|
IEif
of
iexpr
*
iexpr
*
iexpr
|
IEloop
of
loop_annotation
*
iexpr
...
...
src/programs/pgm_types.ml
View file @
852ed2a9
...
...
@@ -228,7 +228,6 @@ module rec T : sig
|
PSlogic
type
psymbol
=
{
(* ps_impure : lsymbol; *)
ps_effect
:
lsymbol
;
ps_pure
:
lsymbol
;
ps_kind
:
psymbol_kind
;
...
...
@@ -352,7 +351,6 @@ end = struct
|
PSlogic
type
psymbol
=
{
(* ps_impure : lsymbol; *)
ps_effect
:
lsymbol
;
ps_pure
:
lsymbol
;
ps_kind
:
psymbol_kind
;
...
...
src/programs/pgm_types.mli
View file @
852ed2a9
...
...
@@ -129,7 +129,6 @@ module rec T : sig
|
PSlogic
type
psymbol
=
{
(* ps_impure : lsymbol; *)
ps_effect
:
lsymbol
;
ps_pure
:
lsymbol
;
ps_kind
:
psymbol_kind
;
...
...
src/programs/pgm_typing.ml
View file @
852ed2a9
...
...
@@ -59,6 +59,25 @@ let () = Exn_printer.register (fun fmt e -> match e with
let
id_result
=
"result"
(* Table of record mutable fields ******************************************)
let
mutable_fields
=
Hts
.
create
17
(* ts -> field:int -> region:int *)
let
declare_mutable_field
ts
i
j
=
Pgm_wp
.
declare_mutable_field
ts
i
j
;
let
h
=
try
Hts
.
find
mutable_fields
ts
with
Not_found
->
let
h
=
Hashtbl
.
create
17
in
Hts
.
add
mutable_fields
ts
h
;
h
in
Hashtbl
.
add
h
i
j
let
mutable_field
ts
i
=
Hashtbl
.
find
(
Hts
.
find
mutable_fields
ts
)
i
let
is_mutable_field
ts
i
=
Hashtbl
.
mem
(
Hts
.
find
mutable_fields
ts
)
i
(* phase 1: typing programs (using destructive type inference) **************)
let
dty_app
(
ts
,
tyl
)
=
assert
(
ts
.
ts_def
=
None
);
tyapp
(
ts
,
tyl
)
...
...
@@ -135,6 +154,9 @@ let check_region_vars () =
List
.
iter
(
fun
h
->
Htv
.
clear
values
;
Htv
.
iter
check
h
)
!
region_vars
;
region_vars
:=
[]
let
is_fresh_region
r
=
r
.
R
.
r_tv
.
tv_name
.
id_string
=
"fresh"
let
rec
specialize_ty
?
(
policy
=
Region_var
)
~
loc
htv
ty
=
match
ty
.
ty_node
with
|
Ty
.
Tyvar
_
->
Denv
.
specialize_ty
~
loc
htv
ty
...
...
@@ -142,7 +164,7 @@ let rec specialize_ty ?(policy=Region_var) ~loc htv ty = match ty.ty_node with
let
n
=
(
get_mtsymbol
ts
)
.
mt_regions
in
let
mk_region
ty
=
match
ty
.
ty_node
with
|
Ty
.
Tyvar
_
when
policy
=
Region_ret
->
tyvar
(
Typing
.
create_user_type_var
"
rho
"
)
tyvar
(
Typing
.
create_user_type_var
"
fresh
"
)
|
Ty
.
Tyvar
tv
when
policy
=
Region_var
->
let
v
=
Denv
.
find_type_var
~
loc
htv
tv
in
push_region_var
tv
(
v
,
loc
);
...
...
@@ -473,9 +495,56 @@ and dexpr_desc ~ghost env loc = function
in
let
d
=
List
.
fold_left2
constructor
d
fl
tyl
in
d
.
dexpr_desc
,
ty
|
Ptree
.
Eassign
_
->
assert
false
(*TODO*)
|
Ptree
.
Eaccess
(
e1
,
q
)
->
let
e1
=
dexpr
~
ghost
env
e1
in
let
x
=
Typing
.
string_list_of_qualid
[]
q
in
let
ls
=
try
ns_find_ls
(
get_namespace
(
impure_uc
env
.
uc
))
x
with
Not_found
->
errorm
~
loc
"unbound record field %a"
print_qualid
q
in
new_regions_vars
()
;
let
ty2
=
match
specialize_lsymbol
~
loc
(
Htv
.
create
17
)
ls
with
|
[
ty1
]
,
Some
ty2
->
expected_type
e1
ty1
;
ty2
|
_
->
assert
false
in
begin
match
Typing
.
is_projection
(
impure_uc
env
.
uc
)
ls
with
|
Some
(
ts
,
_
,
i
)
->
let
mt
=
get_mtsymbol
ts
in
let
j
=
try
Some
(
mutable_field
mt
.
mt_effect
i
)
with
Not_found
->
None
in
DEaccess
(
e1
,
ls
,
j
)
,
ty2
|
_
->
errorm
~
loc
"unbound record field %a"
print_qualid
q
end
|
Ptree
.
Eassign
(
e1
,
q
,
e2
)
->
let
e1
=
dexpr
~
ghost
env
e1
in
let
e2
=
dexpr
~
ghost
env
e2
in
let
x
=
Typing
.
string_list_of_qualid
[]
q
in
let
ls
=
try
ns_find_ls
(
get_namespace
(
impure_uc
env
.
uc
))
x
with
Not_found
->
errorm
~
loc
"unbound record field %a"
print_qualid
q
in
new_regions_vars
()
;
begin
match
specialize_lsymbol
~
loc
(
Htv
.
create
17
)
ls
with
|
[
ty1
]
,
Some
ty2
->
expected_type
e1
ty1
;
expected_type
e2
ty2
|
_
->
assert
false
end
;
begin
match
Typing
.
is_projection
(
impure_uc
env
.
uc
)
ls
with
|
Some
(
ts
,
_
,
i
)
->
let
mt
=
get_mtsymbol
ts
in
let
j
=
try
mutable_field
mt
.
mt_effect
i
with
Not_found
->
errorm
~
loc
"not a mutable field"
in
DEassign
(
e1
,
ls
,
j
,
e2
)
,
dty_unit
env
.
uc
|
None
->
errorm
~
loc
"unbound record field %a"
print_qualid
q
end
|
Ptree
.
Esequence
(
e1
,
e2
)
->
let
e1
=
dexpr
~
ghost
env
e1
in
expected_type
e1
(
dty_unit
env
.
uc
);
...
...
@@ -623,21 +692,6 @@ let region_type ts i =
(* eprintf "%a@." print_mt_symbol mt; *)
Hashtbl
.
find
(
Hts
.
find
region_types
ts
)
i
let
mutable_fields
=
Hts
.
create
17
(* ts -> field:int -> region:int *)
let
declare_mutable_field
ts
i
j
=
Pgm_wp
.
declare_mutable_field
ts
i
j
;
let
h
=
try
Hts
.
find
mutable_fields
ts
with
Not_found
->
let
h
=
Hashtbl
.
create
17
in
Hts
.
add
mutable_fields
ts
h
;
h
in
Hashtbl
.
add
h
i
j
let
mutable_field
ts
i
=
Hashtbl
.
find
(
Hts
.
find
mutable_fields
ts
)
i
let
regions_tyapp
ts
nregions
tyl
=
let
tymatch
s
tv
ty
=
Ty
.
ty_match
s
(
ty_var
tv
)
ty
in
let
s
=
List
.
fold_left2
tymatch
Mtv
.
empty
ts
.
ts_args
tyl
in
...
...
@@ -1043,6 +1097,49 @@ and iexpr_desc gl env loc ty = function
let
env
,
dl
=
iletrec
gl
env
dl
in
let
e1
=
iexpr
gl
env
e1
in
IEletrec
(
dl
,
e1
)
|
DEaccess
(
e1
,
ls
,
j
)
->
let
e1
=
iexpr
gl
env
e1
in
let
x1
=
create_ivsymbol
(
id_fresh
"x"
)
e1
.
iexpr_type
in
let
r
=
match
e1
.
iexpr_type
.
ty_node
,
j
with
|
Ty
.
Tyapp
(
ts
,
tyl
)
,
Some
j
->
let
mt
=
get_mtsymbol
ts
in
let
r
=
regions_tyapp
mt
.
mt_effect
mt
.
mt_regions
tyl
in
Some
(
List
.
nth
r
j
)
|
Ty
.
Tyapp
_
,
None
->
None
|
Ty
.
Tyvar
_
,
_
->
assert
false
in
IElet
(
x1
,
e1
,
mk_iexpr
loc
ty
(
IEaccess
(
x1
,
ls
,
r
)))
|
DEassign
(
e1
,
ls
,
j
,
e2
)
->
(* e1.f <- e2 is syntactic sugar for
let x1 = e1 in let x2 = e2 in any {} writes f { x1.f = x2 } *)
let
e1
=
iexpr
gl
env
e1
in
let
e2
=
iexpr
gl
env
e2
in
let
x1
=
create_ivsymbol
(
id_fresh
"x"
)
e1
.
iexpr_type
in
let
x2
=
create_ivsymbol
(
id_fresh
"x"
)
e2
.
iexpr_type
in
let
r
=
match
e1
.
iexpr_type
.
ty_node
with
|
Ty
.
Tyapp
(
ts
,
tyl
)
->
let
mt
=
get_mtsymbol
ts
in
let
r
=
regions_tyapp
mt
.
mt_effect
mt
.
mt_regions
tyl
in
List
.
nth
r
j
|
Ty
.
Tyvar
_
->
assert
false
in
let
ef
=
{
ie_reads
=
[]
;
ie_writes
=
[
r
];
ie_raises
=
[]
}
in
let
q
=
let
ls
=
(
get_psymbol
ls
)
.
ps_pure
in
t_equ
(
fs_app
ls
[
t_var
x1
.
i_pure
]
x2
.
i_pure
.
vs_ty
)
(
t_var
x2
.
i_pure
)
in
let
q
=
(
create_vsymbol
(
id_fresh
"result"
)
ty
,
q
)
,
[]
in
let
c
=
{
ic_result_type
=
ITpure
ty
;
ic_effect
=
ef
;
ic_pre
=
t_true
;
ic_post
=
q
}
in
IElet
(
x1
,
e1
,
mk_iexpr
loc
ty
(
IElet
(
x2
,
e2
,
mk_iexpr
loc
ty
(
IEany
c
))))
|
DEsequence
(
e1
,
e2
)
->
let
vs
=
create_ivsymbol
(
id_fresh
"_"
)
(
ty_app
(
ts_tuple
0
)
[]
)
in
...
...
@@ -1432,14 +1529,21 @@ and expr_desc gl env loc ty = function
let
env
,
v
=
add_local
env
v
e1
.
expr_type_v
in
let
e2
=
expr
gl
env
e2
in
let
ef
=
E
.
union
e1
.
expr_effect
e2
.
expr_effect
in
if
Sreg
.
exists
(
fun
r
->
occur_type_v
r
e2
.
expr_type_v
)
v
.
pv_regions
then
let
s
=
Sreg
.
filter
is_fresh_region
v
.
pv_regions
in
if
Sreg
.
exists
(
fun
r
->
occur_type_v
r
e2
.
expr_type_v
)
s
then
errorm
~
loc
"local reference would escape its scope"
;
let
ef
=
E
.
remove
v
.
pv_region
s
ef
in
let
ef
=
E
.
remove
s
ef
in
Elet
(
v
,
e1
,
e2
)
,
e2
.
expr_type_v
,
ef
|
IEletrec
(
dl
,
e1
)
->
let
env
,
dl
=
letrec
gl
env
dl
in
let
e1
=
expr
gl
env
e1
in
Eletrec
(
dl
,
e1
)
,
e1
.
expr_type_v
,
e1
.
expr_effect
|
IEaccess
(
i
,
ls
,
r
)
->
let
ef
=
option_apply
E
.
empty
(
fun
r
->
E
.
add_read
r
E
.
empty
)
r
in
let
ls
=
(
get_psymbol
ls
)
.
ps_pure
in
let
v
=
Mvs
.
find
i
.
i_impure
env
in
let
t
=
fs_app
ls
[
t_var
v
.
pv_pure
]
(
purify
ty
)
in
Elogic
t
,
tpure
ty
,
ef
|
IEif
(
e1
,
e2
,
e3
)
->
let
e1
=
expr
gl
env
e1
in
...
...
@@ -1698,7 +1802,7 @@ let type_expr gl e =
let
e
=
iexpr
gl
ienv
e
in
let
e
=
expr
gl
Mvs
.
empty
e
in
check_region_vars
()
;
fresh_expr
gl
~
term
:
true
Spv
.
empty
e
;
(*
fresh_expr gl ~term:true Spv.empty e;
*)
e
let
type_type
uc
ty
=
...
...
@@ -2082,6 +2186,9 @@ let rec decl ~wp env penv ltm lmod uc = function
let
tyv
=
iutype_v
uc
(
create_ienv
denv
)
tyv
in
let
tyv
=
type_v
Mvs
.
empty
tyv
in
if
cannot_be_generalized
tyv
then
errorm
~
loc
"cannot be generalized"
;
if
Debug
.
test_flag
debug
then
eprintf
"@[--parameter %s-----@
\n
%a@]@."
id
.
id
print_type_v
tyv
;
let
ps
,
uc
=
match
tyv
with
|
Tarrow
_
->
let
ps
,
uc
=
add_global_fun
loc
id
.
id
tyv
uc
in
...
...
tests/test-pgm-jcf.mlw
View file @
852ed2a9
module M
use import int.Int
use import module array.Array
use import module ref.Ref
let test (x: ref int) =
{ !x = 0 }
!x
{ result = 0 }
let foo (a: array int) =
{ 1 <= a.length }
a[0] <- 1
{ a[0] = 1 }
(* BUG *)
(*
let foo (a: ref int) = let x = a in fun () -> {} x := 0 { !x = 0 }
let test () = let x = ref 0 in begin foo x (); assert { !x = 0 } end
*)
end
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment