swh:1:snp:6d793aeab171a5710c1817dc2536aa4c79222a27
Tip revision: 1313a7da71c6007248cdb9ac2cb0401946b9d72d authored by François Dupressoir on 14 April 2021, 18:20:13 UTC
Merge remote-tracking branch 'origin/1.0' into deploy-clean-oldmonoid
Merge remote-tracking branch 'origin/1.0' into deploy-clean-oldmonoid
Tip revision: 1313a7d
ecPhlHiAuto.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcUtils
open EcParsetree
open EcFol
open EcModules
open EcCoreGoal
open EcLowGoal
open EcLowPhlGoal
(* -------------------------------------------------------------------- *)
type ll_strategy =
| LL_WP
| LL_RND
| LL_CALL of bool
| LL_JUMP
| LL_COND of ll_strategy list pair
(* -------------------------------------------------------------------- *)
let rec ll_strategy_of_stmt (env : EcEnv.env) (s : stmt) =
List.rev_map (ll_strategy_of_instr env) s.s_node
and ll_strategy_of_instr (env : EcEnv.env) (i : instr) =
match i.i_node with
| Sasgn _ -> LL_WP
| Srnd _ -> LL_RND
| Scall (_, p, _) ->
let p = EcEnv.NormMp.norm_xfun env p in
let proc = EcEnv.Fun.by_xpath p env in
let defn = match proc.f_def with FBdef _ -> true | _ -> false in
LL_CALL defn
| Sif (_, s1, s2) ->
let st1 = ll_strategy_of_stmt env s1 in
let st2 = ll_strategy_of_stmt env s2 in
LL_COND (st1, st2)
| _ -> LL_JUMP
(* -------------------------------------------------------------------- *)
let ll_trivial = EcPhlAuto.t_pl_trivial ~bases:["random"; "lossless"]
(* -------------------------------------------------------------------- *)
let rec apply_ll_strategy (lls : ll_strategy list) tc =
match lls with
| [] ->
t_id tc
| lls1 :: lls ->
FApi.t_last (apply_ll_strategy lls) (apply_ll_strategy1 lls1 tc)
and apply_ll_strategy1 (lls : ll_strategy) tc =
tc |> match lls with
| LL_WP ->
EcPhlWp.t_wp (Some (Single (Zpr.cpos (-1))))
| LL_RND ->
EcPhlRnd.t_bdhoare_rnd PNoRndParams
@> EcPhlConseq.t_bdHoareS_conseq f_true f_true
@~ FApi.t_on1 (-1) ~ttout:ll_trivial t_id
| LL_CALL _ ->
EcPhlCall.t_bdhoare_call f_true f_true None
| LL_JUMP ->
( EcPhlApp.t_bdhoare_app
(Zpr.cpos (-1)) (f_true, f_true, f_r1, f_r1, f_r0, f_r1)
@~ FApi.t_onalli (function
| 1 -> t_id
| 2 -> t_id
| _ -> t_close ll_trivial))
@~ FApi.t_rotate `Left 1
| LL_COND (lls1, lls2) ->
let condtc =
EcPhlCond.t_bdhoare_cond
@+ [apply_ll_strategy lls1; apply_ll_strategy lls2]
in
( EcPhlApp.t_bdhoare_app
(Zpr.cpos (-1)) (f_true, f_true, f_r1, f_r1, f_r0, f_r1)
@~ FApi.t_onalli (function
| 1 -> t_id
| 2 -> condtc
| _ -> t_close ll_trivial))
@~ FApi.t_rotate `Left 1
(* -------------------------------------------------------------------- *)
let t_lossless1_r tc =
let env = FApi.tc1_env tc in
let lls = ll_strategy_of_stmt env (tc1_as_bdhoareS tc).bhs_s in
let tt =
( apply_ll_strategy lls
@~ FApi.t_onall (FApi.t_try EcPhlSkip.t_skip))
@~ FApi.t_onall (EcLowGoal.t_crush ~delta:true) in
let tactic =
(EcPhlConseq.t_bdHoareS_conseq f_true f_true
@~ FApi.t_on1 (-1) ~ttout:ll_trivial
(EcPhlConseq.t_bdHoareS_conseq_bd FHeq f_r1))
@~ FApi.t_on1 (-1) ~ttout:ll_trivial
tt
in FApi.t_onall ll_trivial (tactic tc)
(* -------------------------------------------------------------------- *)
let t_lossless_r tc =
begin
let module E = struct exception InvalidShape end in
let env = FApi.tc1_env tc in
try
match f_node (FApi.tc1_goal tc) with
| FbdHoareF bdf -> begin
let p = EcEnv.NormMp.norm_xfun env bdf.bhf_f in
let proc = EcEnv.Fun.by_xpath p env in
match proc.f_def with FBdef _ -> () | _ -> raise E.InvalidShape
end
| FbdHoareS _ -> ()
| _ -> raise E.InvalidShape
with E.InvalidShape ->
tc_error !!tc "invalid initial goal for `islossless`"
end;
( FApi.t_try EcPhlFun.t_bdhoareF_fun_def
@! t_lossless1_r
@! FApi.t_do `Maybe None
(FApi.t_seq EcPhlFun.t_bdhoareF_fun_def t_lossless1_r)) tc
(* -------------------------------------------------------------------- *)
let t_lossless = FApi.t_low0 "lossless" t_lossless_r