Commit 06c4cb7c authored by Raphaël Rieu-Helft's avatar Raphaël Rieu-Helft

Merge branch 'simp_cast_projections' into 'master'

Simplify projections applied to casted literals in VCs

See merge request !51
parents 6fb58a7a 3356006b
......@@ -20,40 +20,40 @@
<proof prover="5"><result status="valid" time="0.03" steps="11"/></proof>
</goal>
<goal name="VC wmpn_cmp.2" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.05" steps="40"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="39"/></proof>
</goal>
<goal name="VC wmpn_cmp.3" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="47"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="46"/></proof>
</goal>
<goal name="VC wmpn_cmp.4" expl="integer overflow" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="26"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="25"/></proof>
</goal>
<goal name="VC wmpn_cmp.5" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="16"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="15"/></proof>
</goal>
<goal name="VC wmpn_cmp.6" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="28"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="27"/></proof>
</goal>
<goal name="VC wmpn_cmp.7" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.06" steps="28"/></proof>
<proof prover="5"><result status="valid" time="0.06" steps="27"/></proof>
</goal>
<goal name="VC wmpn_cmp.8" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="20"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="19"/></proof>
</goal>
<goal name="VC wmpn_cmp.9" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.06" steps="21"/></proof>
<proof prover="5"><result status="valid" time="0.06" steps="20"/></proof>
</goal>
<goal name="VC wmpn_cmp.10" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="51"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="50"/></proof>
</goal>
<goal name="VC wmpn_cmp.11" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="23"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="22"/></proof>
</goal>
<goal name="VC wmpn_cmp.12" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.07" steps="24"/></proof>
<proof prover="5"><result status="valid" time="0.07" steps="23"/></proof>
</goal>
<goal name="VC wmpn_cmp.13" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
......@@ -61,7 +61,7 @@
<goal name="VC wmpn_cmp.14" expl="assertion" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="VC wmpn_cmp.14.0" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="36"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="35"/></proof>
</goal>
</transf>
</goal>
......@@ -76,11 +76,11 @@
</transf>
</goal>
<goal name="VC wmpn_cmp.16" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.16"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_cmp.17" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="26"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="25"/></proof>
</goal>
<goal name="VC wmpn_cmp.18" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.10"/></proof>
......@@ -88,7 +88,7 @@
<goal name="VC wmpn_cmp.19" expl="assertion" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="VC wmpn_cmp.19.0" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="37"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="36"/></proof>
</goal>
</transf>
</goal>
......@@ -103,20 +103,20 @@
</transf>
</goal>
<goal name="VC wmpn_cmp.21" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="0"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_cmp.22" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="20"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="19"/></proof>
</goal>
<goal name="VC wmpn_cmp.23" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="20"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="19"/></proof>
</goal>
<goal name="VC wmpn_cmp.24" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="44"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="43"/></proof>
</goal>
<goal name="VC wmpn_cmp.25" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="44"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="43"/></proof>
</goal>
<goal name="VC wmpn_cmp.26" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -72,13 +72,13 @@
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_copyi.20" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="212"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="198"/></proof>
</goal>
<goal name="VC wmpn_copyi.21" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_copyi.22" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="98"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="96"/></proof>
</goal>
<goal name="VC wmpn_copyi.23" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
......@@ -99,7 +99,7 @@
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_copyi.29" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="106"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="104"/></proof>
</goal>
<goal name="VC wmpn_copyi.30" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -121,10 +121,10 @@
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_zero_p.3" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC wmpn_zero_p.4" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC wmpn_zero_p.5" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -136,7 +136,7 @@
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_zero_p.8" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="47"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="45"/></proof>
</goal>
<goal name="VC wmpn_zero_p.9" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -148,7 +148,7 @@
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_zero_p.12" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="36"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="35"/></proof>
</goal>
<goal name="VC wmpn_zero_p.13" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -185,10 +185,10 @@
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_zero.8" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.10" steps="106"/></proof>
<proof prover="0"><result status="valid" time="0.10" steps="102"/></proof>
</goal>
<goal name="VC wmpn_zero.9" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="50"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="49"/></proof>
</goal>
<goal name="VC wmpn_zero.10" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
......
......@@ -1513,6 +1513,16 @@ and wp_expr kn k q = match k with
let wp, _, _ = sp_expr kn k Mint.empty Mpv.empty in wp
| Ktag ((Push _|WP), _) -> assert false (* cannot happen *)
let rec simp_cast_projections env t = match t.t_node with
| Tapp (ls, [{t_node = Tconst (Number.ConstInt _ as c);
t_ty = Some {ty_node = Tyapp (ts,_)}}])
when is_range_type_def ts.ts_def
&& ls_equal ls (int_of_range env ts) ->
(* t'int (c:t) -> c *)
t_const c ty_int
| _ ->
t_map (simp_cast_projections env) t
(** VCgen *)
let vc_kode {known_map = kn} vc_wp k =
......@@ -1529,7 +1539,7 @@ let vc_fun env vc_wp cty e =
let vc_rec env vc_wp rdl =
List.map (vc_kode env vc_wp) (k_rec env Mls.empty rdl)
let mk_vc_decl kn id f =
let mk_vc_decl ({known_map = kn} as env) id f =
let {id_string = nm; id_attrs = attrs; id_loc = loc} = id in
let attrs = if attrs_has_expl attrs then attrs else
Sattr.add (Ident.create_attribute ("expl:VC for " ^ nm)) attrs in
......@@ -1537,7 +1547,8 @@ let mk_vc_decl kn id f =
let f = wp_forall (Mvs.keys (t_freevars Mvs.empty f)) f in
let f = Typeinv.inject kn f in
let f = if Debug.test_flag debug_no_eval then f else
Eval_match.eval_match kn f in
Eval_match.eval_match kn f in
let f = simp_cast_projections env f in
create_pure_decl (create_prop_decl Pgoal pr f)
let add_vc_decl kn id f vcl =
......@@ -1552,18 +1563,20 @@ let vc env kn tuc d = match d.pd_node with
| Eexec ({c_node = Cfun e} as c, _) -> c, e
| _ -> c_fun [] [] [] Mxs.empty Mpv.empty e, e in
let f = vc_fun env (Debug.test_noflag debug_sp) c.c_cty e in
add_vc_decl kn v.pv_vs.vs_name f []
add_vc_decl env v.pv_vs.vs_name f []
| PDlet (LDsym (s, {c_node = Cfun e; c_cty = cty})) ->
let env = mk_env env kn tuc in
let f = vc_fun env (Debug.test_noflag debug_sp) cty e in
add_vc_decl kn s.rs_name f []
add_vc_decl env s.rs_name f []
| PDlet (LDrec rdl) ->
let env = mk_env env kn tuc in
let fl = vc_rec env (Debug.test_noflag debug_sp) rdl in
let add rd f vcl = add_vc_decl kn rd.rec_sym.rs_name f vcl in
let add rd f vcl = add_vc_decl env rd.rec_sym.rs_name f vcl in
List.fold_right2 add rdl fl []
| PDtype tdl ->
let env = lazy (mk_env env kn tuc) in
let add_witness d vcl =
let env = Lazy.force env in
let add_fd (mv,ldl) fd e =
let fd = fd_of_rs fd in
let id = id_clone fd.pv_vs.vs_name in
......@@ -1577,16 +1590,16 @@ let vc env kn tuc d = match d.pd_node with
e_let ld e) d.itd_invariant e_void in
let e = List.fold_right e_let ldl e in
let c = c_fun [] [] [] Mxs.empty Mpv.empty e in
let f = vc_fun (mk_env env kn tuc)
(Debug.test_noflag debug_sp) c.c_cty e in
add_vc_decl kn d.itd_its.its_ts.ts_name f vcl in
let f = vc_fun env (Debug.test_noflag debug_sp) c.c_cty e in
add_vc_decl env d.itd_its.its_ts.ts_name f vcl in
let add_invariant d vcl =
let env = Lazy.force env in
let vs_of_rs fd = (fd_of_rs fd).pv_vs in
let vl = List.map vs_of_rs d.itd_fields in
let expl f = vc_expl None Sattr.empty expl_type_inv f in
let f = t_and_asym_l (List.map expl d.itd_invariant) in
let f = t_exists_close_simp vl [] f in
add_vc_decl kn d.itd_its.its_ts.ts_name f vcl in
add_vc_decl env d.itd_its.its_ts.ts_name f vcl in
let add_itd d vcl =
if d.itd_witness <> [] then add_witness d vcl else
if d.itd_invariant <> [] then add_invariant d vcl else
......
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