Skip to content

Commit 9c8b4d9

Browse files
strubstrub
committed
feat(phl): add simplify if tactic
Merges conditional branches that share common code. Also extends `t_code_transform` to eHoare and adds `MatchByPos` branch selection.
1 parent 29e0baa commit 9c8b4d9

12 files changed

Lines changed: 369 additions & 30 deletions

File tree

‎doc/tactics/simplify-if.rst‎

Lines changed: 142 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,142 @@
1+
========================================================================
2+
Tactic: ``simplify if``
3+
========================================================================
4+
5+
The ``simplify if`` transformation performs an if-conversion on program
6+
statements, i.e., it rewrites ``if`` statements into conditional
7+
expressions. This transformation preserves the program semantics.
8+
9+
This conversion helps prevent the weakest precondition from growing
10+
exponentially with the number of ``if`` statements.
11+
12+
To illustrate this issue, consider the following example, which shows
13+
how the weakest precondition can grow exponentially:
14+
15+
.. ecproof::
16+
:title: Weakest precondition grows exponentially.
17+
18+
require import AllCore.
19+
20+
module M = {
21+
proc f (j:int) : int * int = {
22+
var i, x, y;
23+
x <- 0;
24+
y <- 0;
25+
i <- 0;
26+
while (i < 6) {
27+
if (i = j) x <- i;
28+
else y <- y + i;
29+
i <- i + 1;
30+
}
31+
return (x, y);
32+
}
33+
}.
34+
35+
hoare fP j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15).
36+
proof.
37+
proc.
38+
unroll for ^while.
39+
(*$*) time wp. (* The size of the condition grow exponentially in the value of the bound (here 6). *)
40+
skip.
41+
move => />.
42+
smt().
43+
qed.
44+
45+
Since the tactic preserves semantics, it can be applied to all program
46+
logics.
47+
48+
.. admonition:: Syntax
49+
50+
``simplify if side? codepos?``
51+
52+
The ``side`` argument is required when the goal is an ``equiv``
53+
judgment; it specifies on which side the transformation should be
54+
applied. The ``codepos`` argument allows you to indicate which ``if``
55+
statement the transformation should target.
56+
57+
.. contents::
58+
:local:
59+
60+
------------------------------------------------------------------------
61+
Variant: Transform at a given code position
62+
------------------------------------------------------------------------
63+
64+
The tactic applies only if the branches of the selected ``if`` statement
65+
consist solely of assignments.
66+
67+
.. ecproof::
68+
:title: Hoare logic example selecting where to apply the transformation.
69+
70+
require import AllCore.
71+
72+
module M = {
73+
proc f (j:int) : int * int = {
74+
var i, x, y;
75+
x <- 0;
76+
y <- 0;
77+
i <- 0;
78+
while (i < 6) {
79+
if (i = j) x <- i;
80+
else y <- y + i;
81+
i <- i + 1;
82+
}
83+
return (x, y);
84+
}
85+
}.
86+
87+
hoare fP_simplify2 j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15).
88+
proof.
89+
proc.
90+
unroll for ^while.
91+
(* You can select a particular occurence of if using codepos *)
92+
(*$*) simplify if ^if. (* Apply the transformation on the first if *)
93+
simplify if ^if{2}. (* Apply the transformation on the second if *)
94+
simplify if ^if{-2}. (* Apply the trnasformation of the penultimate if *)
95+
time wp.
96+
skip.
97+
move => />.
98+
smt().
99+
qed.
100+
101+
------------------------------------------------------------------------
102+
Variant: Transform as much as possible
103+
------------------------------------------------------------------------
104+
105+
.. admonition:: Syntax
106+
107+
``simplify if``
108+
109+
This variant attempts to find a position where the transformation can
110+
be applied and applies it. The process is repeated until no applicable
111+
position remains.
112+
113+
.. ecproof::
114+
:title: Hoare logic example.
115+
116+
require import AllCore.
117+
118+
module M = {
119+
proc f (j:int) : int * int = {
120+
var i, x, y;
121+
x <- 0;
122+
y <- 0;
123+
i <- 0;
124+
while (i < 6) {
125+
if (i = j) x <- i;
126+
else y <- y + i;
127+
i <- i + 1;
128+
}
129+
return (x, y);
130+
}
131+
}.
132+
133+
hoare fP_simplify j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15).
134+
proof.
135+
proc.
136+
unroll for ^while.
137+
(*$*)simplify if. (* if instruction are transformed into single assignment *)
138+
time wp. (* The size of the wp is now linear in the number of instruction *)
139+
skip.
140+
move => />.
141+
smt().
142+
qed.

‎examples/tactics/simplify_if.ec‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
require import AllCore.
2+
3+
module M = {
4+
proc f (j:int) : int * int = {
5+
var i, x, y;
6+
x <- 0;
7+
y <- 0;
8+
i <- 0;
9+
while (i < 6) {
10+
if (i = j) x <- i;
11+
else y <- y + i;
12+
i <- i + 1;
13+
}
14+
return (x, y);
15+
}
16+
}.
17+
18+
hoare fP j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15).
19+
proof.
20+
proc.
21+
unroll for ^while.
22+
time wp. (* The size of the condition grow exponentially in the value of the bound (here 6). *)
23+
skip.
24+
move => />.
25+
smt().
26+
qed.
27+
28+
hoare fP_simplify j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15).
29+
proof.
30+
proc.
31+
unroll for ^while.
32+
simplify if. (* if instruction are transformed into single assignment *)
33+
time wp. (* The size of the wp is now linear in the number of instruction *)
34+
skip.
35+
move => />.
36+
smt().
37+
qed.
38+
39+
hoare fP_simplify2 j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15).
40+
proof.
41+
proc.
42+
unroll for ^while.
43+
(* You can select a particular occurence of if using codepos *)
44+
simplify if ^if. (* Apply the transformation on the first if *)
45+
simplify if ^if{2}. (* Apply the transformation on the second if *)
46+
simplify if ^if{-2}. (* Apply the trnasformation of the penultimate if *)
47+
time wp.
48+
skip.
49+
move => />.
50+
smt().
51+
qed.

‎src/ecHiTacticals.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -194,6 +194,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
194194
| Pinterleave info -> EcPhlSwap.process_interleave info
195195
| Pcfold info -> EcPhlCodeTx.process_cfold info
196196
| Pkill info -> EcPhlCodeTx.process_kill info
197+
| PsimplifyIf info -> EcPhlCodeTx.process_transform_if info
197198
| Pasgncase info -> EcPhlCodeTx.process_case info
198199
| Palias info -> EcPhlCodeTx.process_alias info
199200
| Pset info -> EcPhlCodeTx.process_set info

‎src/ecLowPhlGoal.ml‎

Lines changed: 13 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -789,7 +789,7 @@ let t_zip f (cenv : code_txenv) (cpos : codepos) (prpo : form * form) (state, s)
789789
((me, Zpr.zip zpr, gs) : memenv * _ * form list)
790790
with InvalidCPos -> tc_error (fst cenv) "invalid code position"
791791

792-
let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc =
792+
let t_code_transform (side : oside) cpos tr tx tc =
793793
let pf = FApi.tc1_penv tc in
794794

795795
match side with
@@ -799,27 +799,32 @@ let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc =
799799
match concl.f_node with
800800
| FhoareS hs ->
801801
let pr, po = hs_pr hs, hs_po hs in
802+
(* FIXME: This is very suspicious why only main is provided ? *)
802803
let po = po.hsi_inv.main in
803804
let (me, stmt, cs) =
804805
tx (pf, hyps) cpos (pr.inv, po) (hs.hs_m, hs.hs_s) in
805806
let concl =
806-
f_hoareS (snd me) (hs_pr hs) stmt (hs_po hs)
807+
f_hoareS (snd me) pr stmt (hs_po hs)
807808
in
808809
FApi.xmutate1 tc (tr None) (cs @ [concl])
809810

810-
| FbdHoareS bhs when bdhoare ->
811+
| FbdHoareS bhs ->
811812
let pr, po = bhs_pr bhs, bhs_po bhs in
812813
let (me, stmt, cs) =
813814
tx (pf, hyps) cpos (pr.inv, po.inv) (bhs.bhs_m, bhs.bhs_s) in
814-
let concl = f_bdHoareS (snd me) (bhs_pr bhs) stmt (bhs_po bhs)
815-
bhs.bhs_cmp (bhs_bd bhs) in
815+
let concl = f_bdHoareS (snd me) pr stmt po bhs.bhs_cmp (bhs_bd bhs) in
816+
FApi.xmutate1 tc (tr None) (cs @ [concl])
817+
818+
| FeHoareS ehs ->
819+
let pr, po = ehs_pr ehs, ehs_po ehs in
820+
let (me, stmt, cs) =
821+
tx (pf, hyps) cpos (pr.inv, po.inv) (ehs.ehs_m, ehs.ehs_s) in
822+
let concl = f_eHoareS (snd me) pr stmt po in
816823
FApi.xmutate1 tc (tr None) (cs @ [concl])
817824

818825
| _ ->
819826
let kinds =
820-
(if bdhoare then [`PHoare `Stmt] else [])
821-
@ [`Hoare `Stmt] in
822-
827+
[`PHoare `Stmt; `Hoare `Stmt; `EHoare `Stmt ] in
823828
tc_error_noXhl ~kinds:kinds pf
824829
end
825830

‎src/ecMatching.ml‎

Lines changed: 40 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ module Position = struct
6868
*)
6969

7070
(* Branch selection *)
71-
type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol]
71+
type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol | `MatchByPos of int]
7272
type nm_codepos_brsel = [`Cond of bool | `Match of int]
7373

7474
(* Linear code position inside a block *)
@@ -354,21 +354,23 @@ module Position = struct
354354
try List.findi (fun _ n -> EcSymbols.sym_equal sel n) cnames |> fst
355355
with Not_found -> raise InvalidCPos
356356

357+
let select_match_arm on_error env e (br:codepos_brsel) =
358+
match br with
359+
| `Match ms -> select_match_arm_idx env e ms
360+
| `MatchByPos ix -> ix
361+
| _ -> on_error ()
362+
357363
(* Get the block pointed to by brsel for a given instruction *)
358364
let normalize_brsel (env: env) (i: instr) (br: codepos_brsel) : (env * stmt) * nm_codepos_brsel =
359365
match i.i_node, br with
360366
| (Sif (_, t, _), `Cond true) -> (env, t), `Cond true
361367
| (Sif (_, _, f), `Cond false) -> (env, f), `Cond false
362368
| (Swhile (_, s), `Cond true) -> (env, s), `Cond true
363-
| (Smatch (e, ss), `Match ms) ->
364-
let ix = select_match_arm_idx env e ms in
369+
| (Smatch (e, ss), _) ->
370+
let ix = select_match_arm (fun _ -> assert false) env e br in
365371
let (locals, s) = List.at ss ix in
366372
let env = EcEnv.Var.bind_locals locals env in
367-
begin try
368-
(env, s), `Match ix
369-
with Invalid_argument _ ->
370-
raise InvalidCPos
371-
end
373+
(env, s), `Match ix
372374
| _ -> assert false
373375

374376
let select_branch (env: env) (i: instr) (br: codepos_brsel) : stmt =
@@ -515,6 +517,34 @@ module Position = struct
515517
let iter_blocks ~(start : nm_codegap1) ~(block_size : int) (s : stmt)
516518
(f : int -> nm_codegap1 -> nm_codegap1 -> unit) : unit =
517519
fold_blocks ~start ~block_size s (fun idx g1 g2 () -> f idx g1 g2) ()
520+
521+
let find_first_matching_instr (test : instr -> bool) (s : stmt) =
522+
let exception Found of codepos in
523+
524+
let rec find_pos rpath n (s : instr list) =
525+
match s with
526+
| [] -> ()
527+
| i :: s ->
528+
if test i then raise (Found (List.rev rpath, cpos1 n));
529+
find_pos_sub rpath n i;
530+
find_pos rpath (n + 1) s
531+
532+
and find_pos_sub rpath n i =
533+
match i.i_node with
534+
| Sif (_, s1, s2) ->
535+
find_pos ((cpos1 n, `Cond true ) :: rpath) 0 s1.s_node;
536+
find_pos ((cpos1 n, `Cond false) :: rpath) 0 s2.s_node
537+
| Swhile (_, s) ->
538+
find_pos ((cpos1 n, `Cond true) :: rpath) 0 s.s_node
539+
| Smatch (_, bs) ->
540+
List.iteri (fun i (_, s) ->
541+
find_pos ((cpos1 n, `MatchByPos i) :: rpath) 0 s.s_node
542+
) bs
543+
| _ -> ()
544+
in
545+
546+
try find_pos [] 0 s.s_node; None
547+
with Found r -> Some r
518548
end
519549

520550
(* -------------------------------------------------------------------- *)
@@ -572,8 +602,8 @@ module Zipper = struct
572602
| Sif (e, ifs1, ifs2), `Cond false ->
573603
(ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2), `Cond false, env
574604

575-
| Smatch (e, bs), `Match cn ->
576-
let ix = select_match_arm_idx env e cn in
605+
| Smatch (e, bs), _ ->
606+
let ix = select_match_arm (fun () -> raise InvalidCPos) env e sub in
577607
let prebr, (locals, body), postbr = List.pivot_at ix bs in
578608
let env = EcEnv.Var.bind_locals locals env in
579609
(ZMatch (e, ((s1, s2), zpr), { locals; prebr; postbr; }), body), `Match ix, env

‎src/ecMatching.mli‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ module Position : sig
3131
]
3232

3333
(* Branch selection *)
34-
type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol]
34+
type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol | `MatchByPos of int]
3535
type nm_codepos_brsel = [`Cond of bool | `Match of int]
3636

3737
(* Linear code position inside a block *)
@@ -218,6 +218,8 @@ module Position : sig
218218
val disjoint : nm_codegap1_range -> nm_codegap1_range -> bool
219219

220220
val nm_codepos1_in_nm_codegap1_range : nm_codepos1 -> nm_codegap1_range -> bool
221+
222+
val find_first_matching_instr : (instr -> bool) -> stmt -> codepos option
221223
end
222224

223225
(* -------------------------------------------------------------------- *)

‎src/ecParser.mly‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3119,6 +3119,9 @@ direction:
31193119
| ALIAS s=side? x=lident CEQ p=sform_h AT o=codepos
31203120
{ Psetmatch (s, o, x, p) }
31213121

3122+
| SIMPLIFY IF s=side? o=codepos?
3123+
{ PsimplifyIf (s, o) }
3124+
31223125
| WEAKMEM s=side? h=loc(ipcore_name) p=param_decl
31233126
{ Pweakmem(s, h, p) }
31243127

‎src/ecParsetree.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -802,6 +802,7 @@ type phltactic =
802802
| Poutline of outline_info
803803
| Pinterleave of interleave_info located
804804
| Pkill of (oside * pcodepos * int option)
805+
| PsimplifyIf of (oside * pcodepos option)
805806
| Pasgncase of (oside * pcodepos)
806807
| Prnd of oside * psemrndpos option * rnd_tac_info_f
807808
| Prndsem of bool * oside * pcodegap1

‎src/ecPrinting.ml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2470,7 +2470,8 @@ let pp_codepos_brsel (fmt: Format.formatter) (br: CP.codepos_brsel) =
24702470
(match br with
24712471
| `Cond true -> "."
24722472
| `Cond false -> "?"
2473-
| `Match cp -> Format.sprintf "#%s." cp)
2473+
| `Match cp -> Format.sprintf "#%s." cp
2474+
| `MatchByPos ix -> Format.sprintf "#%i" ix)
24742475

24752476
let pp_codepos_step (ppe: PPEnv.t) (fmt: Format.formatter) ((cp, br): CP.codepos_step) =
24762477
Format.fprintf fmt "%a%a" (pp_codepos1 ppe) cp pp_codepos_brsel br

0 commit comments

Comments
 (0)