Skip to content

why3
why3
Commit f5c2a483 authored by Raphaël Rieu-Helft's avatar Raphaël Rieu-Helft
Browse files
Options

Fix add_alias; example now works as intended

parent b5b106f9
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 238 additions and 401 deletions
examples/in_progress/alias.mlw
View file @ f5c2a483
......@@ -5,25 +5,22 @@ module Test
mutable f : int;
}
val c1 (x:t) : t
val c (x:t) : t
ensures { x.f = result.f }
alias { x.f ~ result.f }
(*
let test () =
let x = { f = 42 } in
let y = c x in
assert { y.f = 42 };
y.f <- 27;
assert { x.f = 27 };
if any bool then x else y
*)
let c2 (x:t) : unit =
let y = x in
let z = if any bool then x else y in
()
end
module A
use import map.Map
......@@ -55,17 +52,17 @@ module A
val get (p:ptr 'a) : 'a
requires { 0 <= p.offset < plength p }
ensures { result = (p.data)[p.offset] }
(*
let get_ofs (p:ptr 'a) (ofs:int32) : 'a
requires { 0 <= p.offset + Int32.to_int ofs < plength p }
ensures { result = (p.data)[p.offset + Int32.to_int ofs] }
= get (incr p ofs)
*)
val set (p:ptr 'a) (v:'a) : unit
requires { 0 <= p.offset < plength p }
ensures { pelts p = Map.set (pelts (old p)) p.offset v }
writes { p.data.elts }
(*
let set_ofs (p:ptr 'a) (ofs:int32) (v:'a) : unit
requires { 0 <= p.offset + Int32.to_int ofs < plength p }
ensures { pelts p = Map.set (pelts (old p))
......@@ -73,11 +70,10 @@ module A
writes { p.data.elts }
=
set (incr p ofs) v
*)
let test () : unit
=
let zero = Int32.of_int 0 in
let one = Int32.of_int 1 in
let three = UInt32.of_int 3 in
let p = malloc three in
let q = incr p zero in
......
examples/in_progress/alias/why3session.xml 0 → 100644
View file @ f5c2a483
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../alias.mlw" expanded="true">
<theory name="Test" sum="4f615f42994e005c74bb48e590b6e1d2">
<goal name="VC test" expl="VC for test">
<transf name="split_goal_wp">
<goal name="VC test.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC test.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="A" sum="52efc6362ddeccc17cada1f302ec1654">
<goal name="VC get_ofs" expl="VC for get_ofs">
<transf name="split_goal_wp">
<goal name="VC get_ofs.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC get_ofs.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="VC set_ofs" expl="VC for set_ofs">
<transf name="split_goal_wp">
<goal name="VC set_ofs.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC set_ofs.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC test" expl="VC for test">
<transf name="split_goal_wp">
<goal name="VC test.1" expl="1. integer overflow">
<proof prover="0"><result status="valid" time="0.02" steps="72"/></proof>
</goal>
<goal name="VC test.2" expl="2. integer overflow">
<proof prover="0"><result status="valid" time="0.02" steps="73"/></proof>
</goal>
<goal name="VC test.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.03" steps="77"/></proof>
</goal>
<goal name="VC test.4" expl="4. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
</goal>
<goal name="VC test.5" expl="5. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
</goal>
<goal name="VC test.6" expl="6. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="85"/></proof>
</goal>
<goal name="VC test.7" expl="7. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="88"/></proof>
</goal>
<goal name="VC test.8" expl="8. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="88"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
examples/in_progress/mp2.mlw
View file @ f5c2a483
......@@ -12,17 +12,17 @@ module M
use import ref.Ref
type ptr 'a = {
data : ref (array 'a) ;
mutable data : (array 'a) ;
offset : int ;
}
(*invariant { in_us_bounds data.length }*)
(* it is not required the offset is in 0..elts.length *)
function plength (p:ptr 'a) : int
= p.data.contents.length
= p.data.length
function pelts (p:ptr 'a) : int -> 'a
= p.data.contents.elts
= p.data.elts
val p2i (n:int32):int
ensures { result = Int32.to_int n }
......@@ -33,31 +33,30 @@ module M
val null () : ptr 'a
ensures { plength result = 0 }
let incr (p:ptr 'a) (ofs:int32) : ptr 'a
val incr (p:ptr 'a) (ofs:int32) : ptr 'a
ensures { result.offset = p.offset + Int32.to_int ofs }
ensures { result.data = p.data }
=
{ data = p.data; offset = p.offset + p2i ofs }
alias { p.data ~ result.data }
val get (p:ptr 'a) : 'a
requires { 0 <= p.offset < plength p }
ensures { result = !(p.data)[p.offset] }
ensures { result = (p.data)[p.offset] }
let get_ofs (p:ptr 'a) (ofs:int32) : 'a
requires { 0 <= p.offset + Int32.to_int ofs < plength p }
ensures { result = !(p.data)[p.offset + Int32.to_int ofs] }
ensures { result = (p.data)[p.offset + Int32.to_int ofs] }
= get (incr p ofs)
val set (p:ptr 'a) (v:'a) : unit
requires { 0 <= p.offset < plength p }
ensures { pelts p = Map.set (pelts (old p)) p.offset v }
writes { p.data.contents.elts }
writes { p.data.elts }
let set_ofs (p:ptr 'a) (ofs:int32) (v:'a) : unit
requires { 0 <= p.offset + Int32.to_int ofs < plength p }
ensures { pelts p = Map.set (pelts (old p))
(p.offset + Int32.to_int ofs) v }
writes { p.data.contents.elts }
writes { p.data.elts }
=
set (incr p ofs) v
......@@ -107,7 +106,7 @@ module M
ensures { plength result = Int32.to_int sz -> plength p = 0 }
ensures { plength result = Int32.to_int sz ->
forall i:int. 0 <= i < plength (old p) /\ i < Int32.to_int sz ->
!(result.data)[i] = !((old p).data)[i] }
(result.data)[i] = ((old p).data)[i] }
ensures { plength result <> Int32.to_int sz -> p = old p }
......@@ -457,7 +456,7 @@ module N
ensures { value_sub_shift r (p2i sz) + (power radix (p2i sz)) * l2i result =
value_sub_shift x (p2i sz) + l2i y }
ensures { 0 <= l2i result <= 1 }
writes { r.data.contents.elts }
writes { r.data.elts }
=
let limb_zero = UInt32.of_int 0 in
let c = ref y in
......@@ -530,7 +529,7 @@ module N
ensures { 0 <= l2i result <= 1 }
ensures { value_sub_shift r (p2i sz) + (power radix (p2i sz)) * l2i result =
value_sub_shift x (p2i sz) + value_sub_shift y (p2i sz) }
writes { r.data.contents.elts }
writes { r.data.elts }
=
let limb_zero = UInt32.of_int 0 in
let lx = ref limb_zero in
......@@ -592,7 +591,7 @@ module N
ensures { value_sub_shift r (p2i sx) + (power radix (p2i sx)) * l2i result =
value_sub_shift x (p2i sx) + value_sub_shift y (p2i sy) }
ensures { 0 <= l2i result <= 1 }
writes { r.data.contents.elts }
writes { r.data.elts }
=
let limb_zero = UInt32.of_int 0 in
let lx = ref limb_zero in
......@@ -688,7 +687,7 @@ module N
requires { valid_ptr_itv r (p2i sz) }
ensures { value_sub_shift r (p2i sz) + (power radix (p2i sz)) * l2i result
= value_sub_shift x (p2i sz) * l2i y }
writes { r.data.contents.elts }
writes { r.data.elts }
=
let limb_zero = UInt32.of_int 0 in
let lx = ref limb_zero in
......@@ -762,7 +761,7 @@ module N
ensures { value_sub_shift r (p2i sz) + (power radix (p2i sz)) * l2i result
= value_sub_shift (old r) (p2i sz)
+ value_sub_shift x (p2i sz) * l2i y }
writes { r.data.contents.elts }
writes { r.data.elts }
ensures { forall j. j < r.offset \/ r.offset + p2i sz <= j ->
(pelts r)[j] = (pelts (old r))[j] }
=
......@@ -880,7 +879,7 @@ module N
requires { valid_ptr_itv x (p2i sz) }
requires { valid_ptr_itv y (p2i sz) }
requires { valid_ptr_itv r (p2i sz + p2i sz) }
writes { r.data.contents.elts }
writes { r.data.elts }
ensures { value_sub_shift r (p2i sz + p2i sz)
= value_sub_shift x (p2i sz) * value_sub_shift y (p2i sz) }
=
......@@ -1044,7 +1043,7 @@ module N
requires { valid_ptr_itv x (p2i sz) }
requires { valid_ptr_itv y (p2i sz) }
requires { valid_ptr_itv r (p2i sz + p2i sz) }
writes { r.data.contents.elts }
writes { r.data.elts }
ensures { value_sub_shift r (p2i sz + p2i sz)
+ power radix (p2i sz + p2i sz) * l2i result
= value_sub_shift (old r) (p2i sz + p2i sz)
......@@ -1230,7 +1229,7 @@ module N
requires { valid_ptr_itv x (p2i sx) }
requires { valid_ptr_itv y (p2i sy) }
requires { valid_ptr_itv r (p2i sy + p2i sx) }
writes { r.data.contents.elts }
writes { r.data.elts }
ensures { value_sub_shift r (p2i sy + p2i sx)
= value_sub_shift x (p2i sx) * value_sub_shift y (p2i sy) }
=
......
examples/in_progress/mp2/why3session.xml
View file @ f5c2a483
This diff is collapsed.
share/lang/why3.lang
View file @ f5c2a483
......@@ -214,6 +214,7 @@ on linking described in file LICENSE.
</context>
<context id="spec" style-ref="spec-keyword">
<keyword>absurd</keyword>
<keyword>alias</keyword>
<keyword>assert</keyword>
<keyword>assume</keyword>
<keyword>at</keyword>
......
share/latex/why3lang.sty
View file @ f5c2a483
......@@ -5,7 +5,7 @@
\lstdefinelanguage{why3}
{
basicstyle=\ttfamily,%
morekeywords=[1]{abstract,absurd,any,assert,assume,at,axiom,by,%
morekeywords=[1]{abstract,absurd,alias,any,assert,assume,at,axiom,by,%
check,clone,coinductive,constant,diverges,do,done,downto,%
else,end,ensures,exception,exists,export,false,for,forall,fun,%
function,ghost,goal,if,import,in,inductive,invariant,label,lemma,%
......
src/mlw/dexpr.ml
View file @ f5c2a483
......@@ -829,22 +829,35 @@ let effect_of_dspec dsp =
wl, eff
let alias_of_dspec dsp ity =
let add_alias (sbs, regs) (t, rt) = (* FIXME conflicts + result on right *)
let rec subst reg ity2 ity =
match ity.ity_node with
| Ityreg r when reg_equal r reg -> ity2
| Ityapp (s, l, r) ->
ity_app s (List.map (subst reg ity2) l) (List.map (subst reg ity2) r)
| Ityvar _ -> ity
| Ityreg { reg_its = s; reg_args = l; reg_regs = r } -> (* FIXME ? *)
ity_app s (List.map (subst reg ity2) l) (List.map (subst reg ity2) r)
in
let add_alias (ity, regs) (t, rt) =
(* FIXME conflicts *)
match (effect_of_term t, effect_of_term rt) with
| (_, ({ity_node = Ityreg reg} as ity), _),
(_, ({ity_node = Ityreg _} as rity), _) ->
(ity_match sbs ity rity, Sreg.add reg regs)
| (_, ({ity_node = Ityreg reg} as nity), _),
(v, ({ity_node = Ityreg rreg}), _) ->
if v.pv_vs.vs_name.id_string = "result"
then
(subst rreg nity ity, Sreg.add reg regs)
else Loc.errorm ?loc:rt.t_loc "result expected" (* FIXME ? *)
| (_, {ity_node = Ityreg _}, _), _ ->
Loc.errorm ?loc:rt.t_loc "mutable expression expected"
| _ ->
Loc.errorm ?loc:t.t_loc "mutable expression expected" in
let sbs, regs =
let ity, regs =
List.fold_left
add_alias
(ity_match isb_empty ity ity, Sreg.empty)
(ity, Sreg.empty)
dsp.ds_alias in
let ity = ity_full_inst sbs ity in
let regs = Sreg.fold (fun r acc -> reg_freeregs acc r) regs regs in (* FIXME ? *)
let regs = Sreg.fold (fun r acc -> reg_freeregs acc r) regs regs in
(* FIXME ? *)
ity, regs
(* TODO: add warnings for empty postconditions (anywhere)
......@@ -1022,15 +1035,16 @@ let add_binders env pvl = List.fold_left add_pvsymbol env pvl
(** Abstract values *)
let cty_of_spec env bl mask dsp dity =
let cty_of_spec env bl mask dspl dity =
let ity = ity_of_dity dity in
let bl = binders env.ghs bl in
let env = add_binders env bl in
let preold = Mstr.find_opt "0" env.old in
let env, old = add_label env "0" in
let dsp = get_later env dsp ity in
let _, eff = effect_of_dspec dsp in
let dsp = get_later env dspl ity in
let ity, regs = alias_of_dspec dsp ity in
let dsp = get_later env dspl ity in (* FIXME ? *)
let _, eff = effect_of_dspec dsp in
let eff = eff_ghostify env.ghs eff in
let eff = eff_reset_overwritten eff in
let res = Sreg.diff (ity_freeregs Sreg.empty ity) regs in
......
src/tools/why3wc.mll
View file @ f5c2a483
......@@ -91,7 +91,7 @@ let code =
"let" | "val" | "exception"
let annotation =
"requires" | "ensures" | "returns" | "raises" | "reads" | "writes" |
"variant" | "invariant" | "assert" | "assume" | "check"
"variant" | "invariant" | "assert" | "assume" | "check" | "alias"
let digit = ['0'-'9']
let hexadigit = ['0'-'9' 'a'-'f' 'A'-'F']
......
src/why3doc/doc_lexer.mll
View file @ f5c2a483
......@@ -44,7 +44,7 @@
"mutable"; "private"; "raise"; "rec";
"to"; "try"; "val"; "while"; ]
let is_keyword2 = make_table [ "absurd"; "assert"; "assume";
let is_keyword2 = make_table [ "absurd"; "alias"; "assert"; "assume";
"ensures"; "check"; "invariant"; "raises"; "reads"; "requires";
"returns"; "variant"; "writes"; "diverges"; ]
......
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