Skip to content

Commit 78cf6eb

Browse files
strubstrub
committed
Tighten proc-change observability
Restrict proc-change local postconditions to variables observable from the continuation or the goal post, instead of equating all writes from the replaced fragment.
1 parent 7640b32 commit 78cf6eb

5 files changed

Lines changed: 323 additions & 75 deletions

File tree

‎src/ecLowPhlGoal.ml‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -365,6 +365,19 @@ let logicS_read (env : env) (f : logicS) =
365365
| `Equiv hs -> equivS_read env hs
366366
| `EHoare hs -> eHoareS_read env hs
367367

368+
let logicS_post_read (env : env) (f : logicS) =
369+
let add pvs inv = EcPV.form_read env pvs inv in
370+
371+
match f with
372+
| `Hoare hs ->
373+
POE.fold add EcPV.PMVS.empty (hs_po hs).hsi_inv
374+
| `EHoare hs ->
375+
add EcPV.PMVS.empty (ehs_po hs).inv
376+
| `BdHoare hs ->
377+
add (add EcPV.PMVS.empty (bhs_po hs).inv) (bhs_bd hs).inv
378+
| `Equiv es ->
379+
add EcPV.PMVS.empty (es_po es).inv
380+
368381
(* -------------------------------------------------------------------- *)
369382
exception InvalidSplit of codepos1
370383

‎src/ecPV.ml‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ open EcTypes
77
open EcModules
88
open EcFol
99
open EcEnv
10+
open EcMatching
1011

1112
(* -------------------------------------------------------------------- *)
1213
type alias_clash =
@@ -630,6 +631,48 @@ let is_read env is = is_read_r env PV.empty is
630631
let s_read env s = s_read_r env PV.empty s
631632
let f_read env f = f_read_r env PV.empty f
632633

634+
(* -------------------------------------------------------------------- *)
635+
let zpr_pv (kind : [ `Read | `Write ]) (span : [ `Before | `After ]) (env : env) =
636+
let pv_of_stmt =
637+
match kind with
638+
| `Read -> is_read_r
639+
| `Write -> is_write_r ?except:None
640+
in
641+
642+
let rec doit (ctxt : instr option) (pvs : PV.t) (zpr : Zipper.spath) =
643+
let (head, tail), ipath = zpr in
644+
let stail = List.ocons ctxt tail in
645+
let s = stmt (List.rev_append head stail) in
646+
647+
let pvs =
648+
let s = match span with `Before -> head | `After -> tail in
649+
pv_of_stmt env pvs s in
650+
651+
let parent, pvs =
652+
match ipath with
653+
| Zipper.ZTop ->
654+
None, pvs
655+
656+
| Zipper.ZIfThen (e, ps, se) ->
657+
Some (ps, i_if (e, s, se)), pvs
658+
659+
| Zipper.ZIfElse (e, st, ps) ->
660+
Some (ps, i_if (e, st, s)), pvs
661+
662+
| Zipper.ZMatch (e, ps, mpi) ->
663+
let bs =
664+
List.rev_append mpi.prebr ((mpi.locals, s) :: mpi.postbr)
665+
in Some (ps, i_match (e, bs)), pvs
666+
667+
| Zipper.ZWhile (e, ps) ->
668+
let wi = i_while (e, s) in
669+
Some (ps, wi), pv_of_stmt env pvs [wi]
670+
in
671+
672+
ofold (fun (zpr, ctxt) pvs -> doit (Some ctxt) pvs zpr) pvs parent
673+
674+
in fun pvs zpr -> doit None pvs zpr
675+
633676
(* -------------------------------------------------------------------- *)
634677
type pmvs = PV.t Mid.t
635678

‎src/ecPV.mli‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -148,6 +148,15 @@ val is_read : instr list pvaccess0
148148
val s_read : stmt pvaccess0
149149
val f_read : xpath pvaccess0
150150

151+
(* -------------------------------------------------------------------- *)
152+
val zpr_pv :
153+
[ `Read | `Write ]
154+
-> [ `Before | `After ]
155+
-> env
156+
-> PV.t
157+
-> EcMatching.Zipper.spath
158+
-> PV.t
159+
151160
(* -------------------------------------------------------------------- *)
152161
type pmvs = PV.t EcIdent.Mid.t
153162

‎src/phl/ecPhlRewrite.ml‎

Lines changed: 28 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@ open EcCoreGoal
66
open EcEnv
77
open EcModules
88
open EcFol
9-
open EcMatching
109

1110
module L = EcLocation
1211
module PT = EcProofTerm
@@ -230,44 +229,11 @@ let process_rewrite_at
230229
EcPhlConseq.t_conseq pre post tc
231230
|> FApi.t_sub [t_pre; t_post; EcLowGoal.t_id]
232231

233-
(* -------------------------------------------------------------------- *)
234-
let zpr_write (env : env) =
235-
let rec doit (ctxt : instr option) (pvs : EcPV.PV.t) (zpr : Zipper.spath) =
236-
let (head, tail), ipath = zpr in
237-
let tail = List.ocons ctxt tail in
238-
let s = stmt (List.rev_append head tail) in
239-
240-
let pvs = EcPV.is_write_r env pvs head in
241-
242-
let parent, pvs =
243-
match ipath with
244-
| Zipper.ZTop ->
245-
None, pvs
246-
247-
| Zipper.ZIfThen (e, ps, se) ->
248-
Some (ps, i_if (e, s, se)), pvs
249-
250-
| Zipper.ZIfElse (e, st, ps) ->
251-
Some (ps, i_if (e, st, s)), pvs
252-
253-
| Zipper.ZMatch (e, ps, mpi) ->
254-
let bs =
255-
List.rev_append mpi.prebr ((mpi.locals, s) :: mpi.postbr)
256-
in Some (ps, i_match (e, bs)), pvs
257-
258-
| Zipper.ZWhile (e, ps) ->
259-
Some (ps, i_while (e, s)), EcPV.is_write_r env pvs tail
260-
in
261-
262-
ofold (fun (zpr, ctxt) pvs -> doit (Some ctxt) pvs zpr) pvs parent
263-
264-
in fun pvs zpr -> doit None pvs zpr
265-
266232
(* -------------------------------------------------------------------- *)
267233
(* [change] replaces a code range with [s] by generating:
268234
- a local equivalence goal showing that the original fragment and [s]
269235
agree under the framed precondition on the variables they both read,
270-
and produce the same values for everything they may write;
236+
and produce the same values for everything observable afterwards;
271237
- the original program-logic goal with the selected range rewritten. *)
272238
let t_change_stmt
273239
(side : side option)
@@ -284,9 +250,9 @@ let t_change_stmt
284250
(* Collect the variables that may be modified by the surrounding context,
285251
excluding the fragment being replaced. *)
286252
let modi =
287-
let zpr =
288-
(zpr.z_head, List.drop (List.length stmt) zpr.z_tail), zpr.z_path
289-
in zpr_write env EcPV.PV.empty zpr in
253+
let zpr = { zpr with z_tail = epilog } in
254+
let zpr = (zpr.z_head, zpr.z_tail), zpr.z_path in
255+
EcPV.zpr_pv `Write `Before env EcPV.PV.empty zpr in
290256

291257
(* Keep only the top-level conjuncts of the current precondition that talk
292258
about the active memory and are independent from the surrounding writes. *)
@@ -307,8 +273,26 @@ let t_change_stmt
307273
let written = EcPV.is_write_r env written stmt in
308274
let written = EcPV.is_write_r env written s.s_node in
309275

276+
let obs =
277+
let zpr = { zpr with z_tail = epilog } in
278+
let zpr = (zpr.z_head, zpr.z_tail), zpr.z_path in
279+
let obs = EcPV.zpr_pv `Read `After env EcPV.PV.empty zpr in
280+
281+
let goal =
282+
let pvs =
283+
EcLowPhlGoal.logicS_post_read env
284+
(EcLowPhlGoal.get_logicS (FApi.tc1_goal tc))
285+
in
286+
EcIdent.Mid.find_def EcPV.PV.empty (fst me) pvs
287+
in
288+
289+
EcPV.PV.union obs goal
290+
in
291+
292+
let written = EcPV.PV.inter written obs in
293+
310294
(* The local equivalence goal relates shared reads in the precondition and
311-
all possible writes in the postcondition. *)
295+
the writes that remain observable in the continuation/postcondition. *)
312296
let wr_pvs, wr_globs = EcPV.PV.elements written in
313297

314298
let pr_pvs, pr_globs = EcPV.PV.elements @@ EcPV.PV.inter
@@ -337,11 +321,11 @@ let t_change_stmt
337321
(* First subgoal: prove that the replacement fragment preserves the
338322
observable behavior required by the outer proof. *)
339323
let goal1 =
340-
f_equivS
341-
(snd me) (snd me)
342-
{ ml; mr; inv = ofold f_and (f_ands pr_eq) frame; }
343-
(EcAst.stmt stmt) s
344-
{ ml; mr; inv = f_ands po_eq; }
324+
f_equivS
325+
(snd me) (snd me)
326+
{ ml; mr; inv = ofold f_and (f_ands pr_eq) frame; }
327+
(EcAst.stmt stmt) s
328+
{ ml; mr; inv = f_ands po_eq; }
345329
in
346330

347331
let stmt = EcMatching.Zipper.zip { zpr with z_tail = s.s_node @ epilog } in

0 commit comments

Comments
 (0)