New tactic: outline (#473)

The main idea is to provide an inverse to inline when proving an equiv.

Currently, it supports basic procedure unification that requires
manual selection of the program slice to unify with, as well as,
requiring near exact matches on program structure.

An optional return value can be supplied for situations where the
return expression is just a program variable and needs to be
renamed/deconstructed.

There is also support for statement outlining although, this is more
of a transitivity * with program slicing so may require change.

Syntax and variants:

 - Procedure outlining:
   outline {m} [s - e] lv? <@ M.foo

 - Statement outlining:
   outline {m} [s - e] { s1; s2; ... }

with

 - m: 1 or 2
 - s,e: code position
 - M.foo: path to procedure
 - lv: a left-value

when `s = e`, one can use `[s]` instead of `[s-s]`

For example usage see: tests/outline.ec

src/ecCoreModules.ml

@@ -43,6 +43,14 @@ let name_of_lv lv =
   | LvTuple pvs ->
      String.concat "_" (List.map (EcTypes.name_of_pvar |- fst) pvs)
 
+let lv_of_expr e =
+  match e.e_node with
+  | Evar pv ->
+     LvVar (pv, e_ty e)
+  | Etuple pvs ->
+     LvTuple (List.map (fun e -> EcTypes.destr_var e, e_ty e) pvs)
+  | _ -> failwith "failed to construct lv from expr"
+
 (* -------------------------------------------------------------------- *)
 type instr = EcAst.instr
 

src/ecCoreModules.mli

@@ -12,6 +12,7 @@ val ty_of_lv     : lvalue -> EcTypes.ty
 val lv_of_list   : (prog_var * ty) list -> lvalue option
 val lv_to_list   : lvalue -> prog_var list
 val name_of_lv   : lvalue -> string
+val lv_of_expr   : expr -> lvalue
 
 (* --------------------------------------------------------------------- *)
 type instr = EcAst.instr

src/ecHiTacticals.ml

@@ -189,6 +189,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pcallconcave info         -> EcPhlCall.process_call_concave info
     | Pswap sw                  -> EcPhlSwap.process_swap sw
     | Pinline info              -> EcPhlInline.process_inline info
+    | Poutline info             -> EcPhlOutline.process_outline info
     | Pinterleave info          -> EcPhlSwap.process_interleave info
     | Pcfold info               -> EcPhlCodeTx.process_cfold info
     | Pkill info                -> EcPhlCodeTx.process_kill info

src/ecLexer.mll

@@ -154,6 +154,7 @@
     "conseq"      , CONSEQ     ;        (* KW: tactic *)
     "exfalso"     , EXFALSO    ;        (* KW: tactic *)
     "inline"      , INLINE     ;        (* KW: tactic *)
+    "outline"     , OUTLINE    ;        (* KW: tactic *)
     "interleave"  , INTERLEAVE ;        (* KW: tactic *)
     "alias"       , ALIAS      ;        (* KW: tactic *)
     "weakmem"     , WEAKMEM    ;        (* KW: tactic *)

src/ecParser.mly

@@ -512,6 +512,7 @@
 %token NOTATION
 %token OF
 %token OP
+%token OUTLINE
 %token PCENT
 %token PHOARE
 %token PIPE
@@ -3129,6 +3130,10 @@ interleave_info:
 | s=side? c1=interleavepos c2=interleavepos c3=interleavepos* k=word
    { (s, c1, c2 :: c3, k) }
 
+%inline outline_kind:
+| s=brace(stmt) { OKstmt(s) }
+| r=sexpr? LEAT f=loc(fident) { OKproc(f, r) }
+
 phltactic:
 | PROC
    { Pfun `Def }
@@ -3219,6 +3224,14 @@ phltactic:
 | INLINE s=side? u=inlineopt? p=codepos
     { Pinline (`CodePos (s, u, p)) }
 
+| OUTLINE s=side LBRACKET st=codepos1 e=option(MINUS e=codepos1 {e}) RBRACKET k=outline_kind
+    { Poutline {
+	  outline_side  = s; 
+	  outline_start = st; 
+	  outline_end   = odfl st e; 
+	  outline_kind  = k }
+    }
+
 | KILL s=side? o=codepos
     { Pkill (s, o, Some 1) }
 

src/ecParsetree.ml

@@ -670,6 +670,18 @@ type inline_info = [
  (* | `All       of oside * inlineopt *)
 ]
 
+(* -------------------------------------------------------------------- *)
+type outline_kind =
+  | OKstmt of pstmt
+  | OKproc of pgamepath * pexpr option
+
+type outline_info = {
+    outline_side: side;
+    outline_start: codepos1;
+    outline_end: codepos1;
+    outline_kind: outline_kind;
+}
+
 (* -------------------------------------------------------------------- *)
 type fel_info = {
   pfel_cntr  : pformula;
@@ -731,6 +743,7 @@ type phltactic =
   | Pswap          of ((oside * swap_kind) located list)
   | Pcfold         of (oside * codepos * int option)
   | Pinline        of inline_info
+  | Poutline       of outline_info
   | Pinterleave    of interleave_info located
   | Pkill          of (oside * codepos * int option)
   | Prnd           of oside * semrndpos option * rnd_tac_info_f

src/ecUnifyProc.ml

@@ -0,0 +1,115 @@
+open EcAst
+open EcTypes
+open EcModules
+open EcSymbols
+
+(*---------------------------------------------------------------------------------------*)
+type u_error =
+  | UE_InvalidRetInstr
+  | UE_UnexpectedReturn
+  | UE_ExprNotInLockstep of expr * expr
+  | UE_InstrNotInLockstep of instr * instr
+  | UE_DifferentProgramLengths of stmt * stmt
+
+exception UnificationError of u_error
+
+(*---------------------------------------------------------------------------------------*)
+type u_value =
+  | Empty
+  | Fixed of expr
+
+type umap = u_value Msym.t
+
+(*---------------------------------------------------------------------------------------*)
+let rec unify_exprs umap e1 e2 =
+  match e1.e_node, e2.e_node with
+  | Eint _, Eint _ -> umap
+  | Elocal _, Elocal _ -> umap
+  | Evar pv, e2n ->
+     let var = symbol_of_pv pv in
+
+     (* Only update a value if it hasn't been fixed previously *)
+     let update value =
+       match value with
+       | None ->
+          begin
+            match e2n with
+            | Evar _ -> None
+            | _ -> raise (UnificationError (UE_ExprNotInLockstep (e1, e2)))
+          end
+       | Some Empty -> Some (Fixed e2)
+       | _ -> value
+     in
+
+     Msym.change update var umap
+  | Eop _, Eop _ -> umap
+  | Eapp (f1, a1), Eapp (f2, a2) ->
+     let umap = unify_exprs umap f1 f2 in
+     List.fold_left (fun umap (e1, e2) -> unify_exprs umap e1 e2) umap (List.combine a1 a2)
+  | Equant (_, _, e1), Equant (_, _, e2) ->
+     unify_exprs umap e1 e2
+  | Elet (_, e1, u1), Elet (_, e2, u2) ->
+     let umap = unify_exprs umap e1 e2 in
+     unify_exprs umap u1 u2
+  | Etuple t1, Etuple t2 ->
+     List.fold_left (fun umap (e1, e2) -> unify_exprs umap e1 e2) umap (List.combine t1 t2)
+  | Eif (c1, t1, f1), Eif (c2, t2, f2) ->
+     let umap = unify_exprs umap c1 c2 in
+     let umap = unify_exprs umap t1 t2 in
+     unify_exprs umap f1 f2
+  | Ematch (c1, p1, _), Ematch (c2, p2, _) ->
+     let umap = unify_exprs umap c1 c2 in
+     List.fold_left (fun umap (e1, e2) -> unify_exprs umap e1 e2) umap (List.combine p1 p2)
+  | Eproj (e1, _), Eproj (e2, _) ->
+     unify_exprs umap e1 e2
+  | _ -> raise (UnificationError (UE_ExprNotInLockstep (e1, e2)))
+
+(*---------------------------------------------------------------------------------------*)
+let rec unify_instrs umap i1 i2 =
+ match i1.i_node, i2.i_node with
+  | Sasgn(_, e1), Sasgn(_, e2)
+  | Srnd(_, e1), Srnd(_, e2) ->
+     unify_exprs umap e1 e2
+  | Scall(_, _, args1), Scall(_, _, args2) ->
+     List.fold_left (fun umap (e1, e2) -> unify_exprs umap e1 e2) umap (List.combine args1 args2)
+  | Sif(e1, st1, sf1), Sif(e2, st2, sf2) ->
+     let umap = unify_exprs umap e1 e2 in
+     let umap = unify_stmts umap st1 st2 in
+     unify_stmts umap sf1 sf2
+  | Swhile(e1, s1), Swhile(e2, s2) ->
+     let umap = unify_exprs umap e1 e2 in
+     unify_stmts umap s1 s2
+  | Smatch(e1, bs1), Smatch(e2, bs2) ->
+     let umap = unify_exprs umap e1 e2 in
+     List.fold_left (fun umap (b1, b2) -> unify_stmts umap (snd b1) (snd b2)) umap (List.combine bs1 bs2)
+  | Sassert e1, Sassert e2 ->
+     unify_exprs umap e1 e2
+  | Sabstract _, Sabstract _ -> umap
+  | _ -> raise (UnificationError (UE_InstrNotInLockstep (i1, i2)));
+
+and unify_stmts umap s1 s2 =
+  let s1n, s2n = s1.s_node, s2.s_node in
+  if List.length s1n <> List.length s2n then
+    raise (UnificationError (UE_DifferentProgramLengths (s1, s2)));
+  List.fold_left (fun umap (i1, i2) -> unify_instrs umap i1 i2) umap (List.combine s1n s2n)
+
+(*---------------------------------------------------------------------------------------*)
+(* Given a function definition attempt to unify its body with the statements `sb` 
+   and if a return statement is given, also unify it's expression. *)
+let unify_func umap fdef sb sr =
+  (* Unify the body *)
+  let umap = unify_stmts umap fdef.f_body sb in
+
+  (* Unify the return stmt (if it exists) and retrieve its lv *)
+  match sr with
+  | Some i -> begin
+      (* Check that there is a return expression to unify with *)
+      if fdef.f_ret = None then
+        raise (UnificationError UE_UnexpectedReturn);
+
+      (* Only unify with assignment instructions *)
+      match i.i_node with
+      | Sasgn (lv, e) -> Some lv, unify_exprs umap (Option.get fdef.f_ret) e
+      | _ -> raise (UnificationError UE_InvalidRetInstr)
+  end
+  | _ -> None, umap

src/ecUnifyProc.mli

@@ -0,0 +1,43 @@
+open EcTypes
+open EcModules
+open EcSymbols
+
+(*---------------------------------------------------------------------------------------*)
+(* `Unification` of procedures *)
+(*
+  Given: r <@ foo(a1: t1, a2: t2, ...); and s1; s2; ...; sr.
+  Attempt to find values for a1, a2, ... such that, the body of `foo` with a1, a2, ...
+  replaced will exactly match s1; s2; ..., and that `r <- res` match sr.
+  Where `res` is the return expression of `foo`.
+
+  Currently, this is done by traversing the respective ASTs and when a relevant
+  program variable is encountered on the lhs, use the rhs expression.
+
+  FIXME: This is incredibly basic and should be iterated on with a more advanced
+  procedure unification algorithm.
+ *)
+
+(*---------------------------------------------------------------------------------------*)
+type u_error =
+  | UE_InvalidRetInstr
+  | UE_UnexpectedReturn
+  | UE_ExprNotInLockstep of expr * expr
+  | UE_InstrNotInLockstep of instr * instr
+  | UE_DifferentProgramLengths of stmt * stmt
+
+exception UnificationError of u_error
+
+(*---------------------------------------------------------------------------------------*)
+type u_value =
+  | Empty
+  | Fixed of expr
+
+type umap = u_value Msym.t
+
+(*---------------------------------------------------------------------------------------*)
+(* The following functions attempt to unify unknown program variables
+   in the lhs with expressions from the rhs *)
+val unify_exprs : umap -> expr -> expr -> umap
+val unify_instrs : umap -> instr -> instr -> umap
+val unify_stmts : umap -> stmt -> stmt -> umap
+val unify_func : umap -> function_def -> stmt -> instr option -> lvalue option * umap