Alias sub-expressions in statements

strub · strub · commit ad2615baf3f7 · 2024-10-29T14:10:05.000+01:00
The tactic `alias $name := $pattern @ $pos` alias the $pattern (subject
to matching) in the instruction targetted by $pos using a fresh
program variable $name.

The tactic does not apply to the expression contained in the
condition of a while loop.
diff --git a/src/ecCoreModules.ml b/src/ecCoreModules.ml
@@ -232,6 +232,19 @@ and i_get_uninit_read (w : Ssym.t) (i : instr) =
 let get_uninit_read (s : stmt) =
   snd (s_get_uninit_read Ssym.empty s)
 
+
+(* -------------------------------------------------------------------- *)
+type instr_with_expr = [`Sasgn | `Srnd | `Sif | `Smatch | `Swhile]
+
+let get_expression_of_instruction (i : instr) : (_ * instr_with_expr * _) option =
+  match i.i_node with
+  | Sasgn  (lv, e)     -> Some (e, `Sasgn , (fun e -> i_asgn  (lv, e)))
+  | Srnd   (lv, e)     -> Some (e, `Srnd  , (fun e -> i_rnd   (lv, e)))
+  | Sif    (e, s1, s2) -> Some (e, `Sif   , (fun e -> i_if    (e, s1, s2)))
+  | Swhile (e, s)      -> Some (e, `Swhile, (fun e -> i_while (e, s)))
+  | Smatch (e, bs)     -> Some (e, `Smatch, (fun e -> i_match (e, bs)))
+  | _                  -> None
+
 (* -------------------------------------------------------------------- *)
 type 'a use_restr = 'a EcAst.use_restr
 
diff --git a/src/ecCoreModules.mli b/src/ecCoreModules.mli
@@ -79,6 +79,11 @@ val is_assert : instr -> bool
 (* -------------------------------------------------------------------- *)
 val get_uninit_read : stmt -> Sx.t
 
+(* -------------------------------------------------------------------- *)
+type instr_with_expr = [`Sasgn | `Srnd | `Sif | `Smatch | `Swhile]
+
+val get_expression_of_instruction : instr -> (expr * instr_with_expr * (expr -> instr)) option
+
 (* -------------------------------------------------------------------- *)
 type funsig = {
   fs_name   : symbol;
diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml
@@ -196,6 +196,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pasgncase info            -> EcPhlCodeTx.process_case info
     | Palias info               -> EcPhlCodeTx.process_alias info
     | Pset info                 -> EcPhlCodeTx.process_set info
+    | Psetmatch info            -> EcPhlCodeTx.process_set_match info
     | Pweakmem info             -> EcPhlCodeTx.process_weakmem info
     | Prnd (side, pos, info)    -> EcPhlRnd.process_rnd side pos info
     | Prndsem (red, side, pos)  -> EcPhlRnd.process_rndsem ~reduce:red side pos
diff --git a/src/ecParser.mly b/src/ecParser.mly
@@ -3098,6 +3098,9 @@ interleave_info:
 | ALIAS s=side? o=codepos x=lident EQ e=expr
     { Pset (s, o, false, x,e) }
 
+| ALIAS s=side? x=lident CEQ p=sform_h AT o=codepos
+    { Psetmatch (s, o, x, p) }
+
 | WEAKMEM s=side? h=loc(ipcore_name) p=param_decl
     { Pweakmem(s, h, p) }
 
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
@@ -745,6 +745,7 @@ type phltactic =
   | Palias         of (oside * pcodepos * osymbol_r)
   | Pweakmem       of (oside * psymbol * fun_params)
   | Pset           of (oside * pcodepos * bool * psymbol * pexpr)
+  | Psetmatch      of (oside * pcodepos * psymbol * pformula)
   | Pconseq        of (pcqoptions * (conseq_ppterm option tuple3))
   | Pconseqauto    of crushmode
   | Pconcave       of (pformula option tuple2 gppterm * pformula)
diff --git a/src/ecUtils.ml b/src/ecUtils.ml
@@ -467,6 +467,10 @@ module List = struct
 
   include Parallel
 
+  (* ------------------------------------------------------------------ *)
+  let destruct (s : 'a list) =
+    match s with x :: xs -> (x, xs) | _ -> assert false
+
   (* ------------------------------------------------------------------ *)
   let nth_opt (s : 'a list) (i : int) =
     try  Some (List.nth s i)
diff --git a/src/ecUtils.mli b/src/ecUtils.mli
@@ -281,6 +281,7 @@ module List : sig
   val min : ?cmp:('a -> 'a -> int) -> 'a list -> 'a
   val max : ?cmp:('a -> 'a -> int) -> 'a list -> 'a
 
+  val destruct   : 'a list -> 'a * 'a list
   val nth_opt    : 'a list -> int -> 'a option
   val mbfilter   : ('a -> bool) -> 'a list -> 'a list
   val fusion     : ('a -> 'a -> 'a) -> 'a list -> 'a list -> 'a list
diff --git a/src/phl/ecPhlCodeTx.ml b/src/phl/ecPhlCodeTx.ml
@@ -1,12 +1,14 @@
 (* -------------------------------------------------------------------- *)
 open EcUtils
 open EcParsetree
+open EcSymbols
 open EcAst
 open EcTypes
 open EcModules
 open EcFol
 open EcEnv
 open EcPV
+open EcMatching
 
 open EcCoreGoal
 open EcLowPhlGoal
@@ -136,6 +138,51 @@ let t_set_r side cpos (fresh, id) e tc =
   let tr = fun side -> `Set (side, cpos) in
   t_code_transform side ~bdhoare:true cpos tr (t_zip (set_stmt (fresh, id) e)) tc
 
+(* -------------------------------------------------------------------- *)
+let set_match_stmt (id : symbol) ((ue, mev, ptn) : _ * _ * form) =
+  fun (pe, hyps) _ me z ->
+    let i, is = List.destruct z.Zpr.z_tail in
+    let e, mk =
+      let e, kind, mk =
+        get_expression_of_instruction i |> ofdfl (fun () ->
+          tc_error pe "targetted instruction should contain an expression"
+        ) in
+
+      match kind with
+      | `Sasgn | `Srnd | `Sif | `Smatch -> (e, mk)
+      | `Swhile -> tc_error pe "while loops not supported"
+    in
+
+    try
+      let ptev = EcProofTerm.ptenv pe hyps (ue, mev) in
+      let e = form_of_expr (fst me) e in
+      let subf, occmode = EcProofTerm.pf_find_occurence_lazy ptev ~ptn e in
+
+      assert (EcProofTerm.can_concretize ptev);
+
+      let cpos =
+        EcMatching.FPosition.select_form
+          ~xconv:`AlphaEq ~keyed:occmode.k_keyed
+          hyps None subf e in
+
+      let v = { ov_name = Some id; ov_type = subf.f_ty } in
+      let (me, id) = EcMemory.bind_fresh v me in
+      let pv = pv_loc (oget id.ov_name) in
+      let e = EcMatching.FPosition.map cpos (fun _ -> f_pvar pv (subf.f_ty) (fst me)) e in
+
+      let i1 = i_asgn (LvVar (pv, subf.f_ty), expr_of_form (fst me) subf) in
+      let i2 = mk (expr_of_form (fst me) e) in
+
+      (me, { z with z_tail = i1 :: i2 :: is }, [])
+
+    with EcProofTerm.FindOccFailure _ ->
+      tc_error pe "cannot find an occurrence of the pattern"
+
+let t_set_match_r (side : oside) (cpos : Position.codepos) (id : symbol) pattern tc =
+  let tr = fun side -> `SetMatch (side, cpos) in
+  t_code_transform side ~bdhoare:true cpos tr
+    (t_zip (set_match_stmt id pattern)) tc
+
 (* -------------------------------------------------------------------- *)
 let cfold_stmt ?(simplify = true) (pf, hyps) (me : memenv) (olen : int option) (zpr : Zpr.zipper) =
   let env =  LDecl.toenv hyps in
@@ -286,10 +333,11 @@ let t_cfold_r side cpos olen g =
   t_code_transform side ~bdhoare:true cpos tr (t_zip cb) g
 
 (* -------------------------------------------------------------------- *)
-let t_kill  = FApi.t_low3 "code-tx-kill"  t_kill_r
-let t_alias = FApi.t_low3 "code-tx-alias" t_alias_r
-let t_set   = FApi.t_low4 "code-tx-set"   t_set_r
-let t_cfold = FApi.t_low3 "code-tx-cfold" t_cfold_r
+let t_kill      = FApi.t_low3 "code-tx-kill"      t_kill_r
+let t_alias     = FApi.t_low3 "code-tx-alias"     t_alias_r
+let t_set       = FApi.t_low4 "code-tx-set"       t_set_r
+let t_set_match = FApi.t_low4 "code-tx-set-match" t_set_match_r
+let t_cfold     = FApi.t_low3 "code-tx-cfold"     t_cfold_r
 
 (* -------------------------------------------------------------------- *)
 let process_cfold (side, cpos, olen) tc =
@@ -309,8 +357,18 @@ let process_set (side, cpos, fresh, id, e) tc =
   let cpos = EcProofTyping.tc1_process_codepos tc (side, cpos) in
   t_set side cpos (fresh, id) e tc
 
+let process_set_match (side, cpos, id, pattern) tc =
+  let cpos = EcProofTyping.tc1_process_codepos tc (side, cpos) in
+  let me, _ = tc1_get_stmt side tc in
+  let hyps = LDecl.push_active me (FApi.tc1_hyps tc) in
+  let ue  = EcProofTyping.unienv_of_hyps hyps in
+  let ptnmap = ref Mid.empty in
+  let pattern = EcTyping.trans_pattern (LDecl.toenv hyps) ptnmap ue pattern in
+  t_set_match side cpos (EcLocation.unloc id)
+    (ue, EcMatching.MEV.of_idents (Mid.keys !ptnmap) `Form, pattern)
+    tc
+  
 (* -------------------------------------------------------------------- *)
-
 let process_weakmem (side, id, params) tc =
   let open EcLocation in
   let hyps = FApi.tc1_hyps tc in
diff --git a/src/phl/ecPhlCodeTx.mli b/src/phl/ecPhlCodeTx.mli
@@ -1,21 +1,26 @@
 (* -------------------------------------------------------------------- *)
 open EcParsetree
-open EcTypes
+open EcSymbols
+open EcAst
 open EcCoreGoal.FApi
 open EcMatching.Position
+open EcMatching
+open EcUnify
 
 (* -------------------------------------------------------------------- *)
-val t_kill  : oside -> codepos -> int option -> backward
-val t_alias : oside -> codepos -> psymbol option -> backward
-val t_set   : oside -> codepos -> bool * psymbol -> expr -> backward
-val t_cfold : oside -> codepos -> int option -> backward
+val t_kill      : oside -> codepos -> int option -> backward
+val t_alias     : oside -> codepos -> psymbol option -> backward
+val t_set       : oside -> codepos -> bool * psymbol -> expr -> backward
+val t_set_match : oside -> codepos -> symbol -> unienv * mevmap * form -> backward
+val t_cfold     : oside -> codepos -> int option -> backward
 
 (* -------------------------------------------------------------------- *)
-val process_kill  : oside * pcodepos * int option -> backward
-val process_alias : oside * pcodepos * psymbol option -> backward
-val process_set   : oside * pcodepos * bool * psymbol * pexpr -> backward
-val process_cfold : oside * pcodepos * int option -> backward
-val process_case  : oside * pcodepos -> backward
+val process_kill      : oside * pcodepos * int option -> backward
+val process_alias     : oside * pcodepos * psymbol option -> backward
+val process_set       : oside * pcodepos * bool * psymbol * pexpr -> backward
+val process_set_match : oside * pcodepos * psymbol * pformula -> backward
+val process_cfold     : oside * pcodepos * int option -> backward
+val process_case      : oside * pcodepos -> backward
 
 (* -------------------------------------------------------------------- *)
 val process_weakmem : (oside * psymbol * fun_params) -> backward
diff --git a/src/phl/ecPhlRewrite.ml b/src/phl/ecPhlRewrite.ml
@@ -6,16 +6,6 @@ open EcEnv
 open EcModules
 open EcFol
 
-(* -------------------------------------------------------------------- *)
-let get_expression_of_instruction (i : instr) =
-  match i.i_node with
-  | Sasgn  (lv, e)     -> Some (e, (fun e -> i_asgn  (lv, e)))
-  | Srnd   (lv, e)     -> Some (e, (fun e -> i_rnd   (lv, e)))
-  | Sif    (e, s1, s2) -> Some (e, (fun e -> i_if    (e, s1, s2)))
-  | Swhile (e, s)      -> Some (e, (fun e -> i_while (e, s)))
-  | Smatch (e, bs)     -> Some (e, (fun e -> i_match (e, bs)))
-  | _                  -> None
-
 (* -------------------------------------------------------------------- *)
 let t_change
     (side : side option)
@@ -26,12 +16,11 @@ let t_change
   let hyps, concl = FApi.tc1_flat tc in
 
   let change (m : memenv) (i : instr) =
-    let e, mk =
+    let e, _, mk =
       EcUtils.ofdfl
         (fun () ->
            tc_error !!tc
-             "targeted instruction should be \
-             an assignment or random sampling")
+             "targetted instruction should contain an expression")
         (get_expression_of_instruction i)
     in
 
diff --git a/tests/alias-subexpr-with-matching.ec b/tests/alias-subexpr-with-matching.ec
@@ -0,0 +1,33 @@
+require import AllCore.
+
+op foo : int -> int.
+op bar : int -> int distr.
+
+module M = {
+  proc f() : int = {
+    return 0;
+  }
+
+  proc g() = {
+    var x : int;
+
+    x <- foo (5 + 3);
+    x <$ bar (x + 2);
+
+    while (2 * x < 4) {
+    }
+
+    x <@ f();
+  }
+}.
+
+
+lemma L : hoare[M.g : true ==> true].
+proof.
+proc.
+alias c := (_ + 3) @ 1.
+alias d := (x + _) @ 3.
+
+fail alias e := (_ * x) @ ^ while.
+fail alias e := 3 @ ^ <@.
+abort.
