New vernacular command: eval

Target: evaluation of pWhile programs.

Author: strub

src/ecCommands.ml

@@ -630,6 +630,37 @@ and process_dump scope (source, tc) =
 
   scope
 
+(* -------------------------------------------------------------------- *)
+and process_eval (scope : EcScope.scope) ((f, args) : pgamepath * pexpr list) =
+  let env = EcScope.env scope in
+  let fpath = EcTyping.trans_gamepath env f in
+  let fun_  = EcEnv.Fun.by_xpath fpath env in
+  let args =
+    let ue = EcUnify.UniEnv.create None in
+    let args, _ = EcTyping.trans_args env ue f.pl_loc fun_.f_sig args in
+    if not (EcUnify.UniEnv.closed ue) then
+      EcScope.hierror "cannot infer all type variables";
+    let subst = EcUnify.UniEnv.close ue in
+    let subst = EcCoreSubst.Tuni.subst subst in
+    let args = List.map (EcCoreSubst.e_subst subst) args in
+    args
+  in
+
+  let aout = EcProcEval.eval env (fpath, args) in
+  
+  begin
+    match aout with
+    | None ->
+      EcScope.notify scope `Warning
+        "%s" "cannot compute a concrete value"
+
+  | Some aout ->
+    let ppe = EcPrinting.PPEnv.ofenv env in
+    EcScope.notify scope `Info "%a" (EcPrinting.pp_expr ppe) aout
+  end;
+
+  scope
+
 (* -------------------------------------------------------------------- *)
 and process (ld : Loader.loader) (scope : EcScope.scope) g =
   let loc = g.pl_loc in
@@ -672,6 +703,7 @@ and process (ld : Loader.loader) (scope : EcScope.scope) g =
       | Greduction   red  -> `Fct   (fun scope -> process_reduction  scope red)
       | Ghint        hint -> `Fct   (fun scope -> process_hint       scope hint)
       | GdumpWhy3    file -> `Fct   (fun scope -> process_dump_why3  scope file)
+      | Geval        call -> `Fct   (fun scope -> process_eval       scope call)
     with
     | `Fct   f -> Some (f scope)
     | `State f -> f scope; None

src/ecLexer.mll

@@ -208,6 +208,7 @@
     "dump"        , DUMP       ;        (* KW: global *)
     "remove"      , REMOVE     ;        (* KW: global *)
     "exit"        , EXIT       ;        (* KW: global *)
+    "eval"        , EVAL       ;        (* KW: global *)
 
     "fail"        , FAIL       ;        (* KW: internal *)
     "time"        , TIME       ;        (* KW: internal *)

src/ecModules.mli

@@ -36,4 +36,4 @@ val mr_add_restr :
 
 val change_oicalls : oracle_infos -> string -> xpath list -> oracle_infos
 
-val oicalls_filter : oracle_infos -> string -> (xpath -> bool) -> oracle_infos
+val oicalls_filter : oracle_infos -> string -> (xpath -> bool) -> oracle_infos

src/ecParser.mly

@@ -438,6 +438,7 @@
 %token EQ
 %token EQUIV
 %token ETA
+%token EVAL
 %token EXACT
 %token EXFALSO
 %token EXIST
@@ -3811,6 +3812,12 @@ user_red_option:
 (* Search pattern                                                       *)
 %inline search: x=sform_h { x }
 
+(* -------------------------------------------------------------------- *)
+(* Evaluation                                                           *)
+eval:
+| EVAL mp=loc(fident) args=paren(plist0(expr, COMMA))
+    { (mp, args) }
+
 (* -------------------------------------------------------------------- *)
 (* Global entries                                                       *)
 
@@ -3848,6 +3855,7 @@ global_action:
 | SEARCH x=search+ { Gsearch      x  }
 | LOCATE x=qident  { Glocate      x  }
 | WHY3 x=STRING    { GdumpWhy3    x  }
+| eval             { Geval        $1 }
 
 | PRAGMA       x=pragma { Gpragma x }
 | PRAGMA PLUS  x=pragma { Goption (x, `Bool true ) }

src/ecParsetree.ml

@@ -1265,6 +1265,7 @@ type global_action =
   | Gpragma      of psymbol
   | Goption      of (psymbol * [`Bool of bool | `Int of int])
   | GdumpWhy3    of string
+  | Geval        of (pgamepath * pexpr list)
 
 type global = {
   gl_action : global_action located;

src/ecProcEval.ml

@@ -0,0 +1,120 @@
+(* -------------------------------------------------------------------- *)
+open EcUtils
+open EcPath
+open EcAst
+
+(* -------------------------------------------------------------------- *)
+let eval (env : EcEnv.env) =
+  let exception NotAValue in
+
+  let hyps = EcEnv.LDecl.init env [] in
+  let cbv  = EcCallbyValue.norm_cbv EcReduction.full_red hyps in 
+
+  let rec get_function (fpath : xpath) =
+    let fun_ = EcEnv.Fun.by_xpath fpath env in
+
+    match fun_.f_def with
+    | FBdef def -> fun_, def
+    | FBalias alias -> let _, def = get_function alias in fun_, def
+    | _ -> raise NotAValue in
+
+  let rec is_literal (f : form) =
+    match EcFol.sform_of_form f with
+    | SFtrue | SFfalse | SFint _ -> true
+    | SFtuple fs -> List.for_all is_literal fs
+    | _ -> false in
+
+  let eval (subst : EcPV.PVM.subst) (v : form) =
+    let aout = cbv (EcPV.PVM.subst env subst v) in
+    if not (is_literal aout) then raise NotAValue;
+    aout in
+
+  let rec doit (fpath : xpath) (args : form list) =
+    let fun_, body = get_function fpath in
+    let subst =
+      List.fold_left2 (fun (subst : EcPV.PVM.subst) (var : ovariable) (arg : form) ->
+        var.ov_name |> Option.fold ~none:subst ~some:(fun name ->
+          let pv = EcTypes.pv_loc name in
+          EcPV.PVM.add env pv mhr arg subst
+        )
+      ) EcPV.PVM.empty fun_.f_sig.fs_anames args in
+
+    let subst = for_stmt subst body.f_body in
+
+    Option.map
+      (eval subst -| EcFol.form_of_expr mhr)
+      body.f_ret
+  
+  and for_instr (subst : EcPV.PVM.subst) (instr : EcModules.instr) = 
+    match instr.i_node with
+    | Sasgn (lvalue, rvalue) -> begin
+      let rvalue = eval subst (EcFol.form_of_expr mhr rvalue) in
+      match lvalue with
+      | LvVar (pv, _) ->
+        EcPV.PVM.add env pv mhr rvalue subst
+      | LvTuple pvs ->
+        let rvalue = EcFol.destr_tuple rvalue in
+        List.fold_left2 (fun subst (pv, _) rvalue ->
+          EcPV.PVM.add env pv mhr rvalue subst
+        ) subst pvs rvalue
+    end
+
+    | Scall (lv, f, args) -> begin
+      let args = List.map (eval subst -| EcFol.form_of_expr mhr) args in
+      let aout = doit f args in
+
+      match lv with
+      | None ->
+        subst
+
+      | Some (LvVar (pv, _)) ->
+        EcPV.PVM.add env pv mhr (Option.get aout) subst
+
+      | Some (LvTuple pvs) ->
+        List.fold_left2 (fun subst (pv, _) aout ->
+          EcPV.PVM.add env pv mhr aout subst
+        ) subst pvs (EcFol.destr_tuple (Option.get aout))
+    end
+
+    | Sif (cond, strue, sfalse) ->
+      let cond = eval subst (EcFol.form_of_expr mhr cond) in
+      let branch =
+        match EcFol.sform_of_form cond with
+        | SFtrue  -> strue
+        | SFfalse -> sfalse
+        | _ -> raise NotAValue in
+
+      for_stmt subst branch
+
+    | Swhile (cond, body) -> begin
+      let cond = eval subst (EcFol.form_of_expr mhr cond) in
+
+      match EcFol.sform_of_form cond with
+      | SFtrue ->
+        let subst = for_stmt subst body in
+        let subst = for_instr subst instr in
+        subst
+
+      | SFfalse ->
+        subst
+
+      | _ ->
+        raise NotAValue
+      end
+
+    | Sabstract _
+    | Sassert   _
+    | Smatch    _
+    | Srnd      _ -> raise NotAValue
+
+    and for_stmt (subst : EcPV.PVM.subst) (stmt : stmt) =
+    List.fold_left for_instr subst stmt.s_node
+
+  in
+
+  fun ((fpath, args) : xpath * expr list) ->
+    try
+      let aout =
+        doit fpath (List.map (cbv -| EcFol.form_of_expr mhr) args)
+      in Option.map (EcFol.expr_of_form mhr) aout
+    with NotAValue -> None

src/ecProcEval.mli

@@ -0,0 +1,6 @@
+(* -------------------------------------------------------------------- *)
+open EcPath
+open EcAst
+
+(* -------------------------------------------------------------------- *)
+val eval : EcEnv.env -> xpath * expr list -> expr option

src/ecTyping.ml

@@ -1657,6 +1657,7 @@ let transcall transexp env ue loc fsig args =
   in
     (args, fsig.fs_ret)
 
+(* -------------------------------------------------------------------- *)
 let trans_args env ue = transcall (transexp env `InProc ue) env ue
 
 (* -------------------------------------------------------------------- *)

src/ecTyping.mli

@@ -234,6 +234,25 @@ val trans_pattern  : env -> ptnmap -> EcUnify.unienv -> pformula -> EcFol.form
 val trans_memtype :
   env -> EcUnify.unienv -> pmemtype -> EcMemory.memtype
 
+(* -------------------------------------------------------------------- *)
+val transcall :
+     ('a located -> 'b * ty)
+  -> EcEnv.env
+  -> EcUnify.unienv
+  -> EcLocation.t
+  -> EcModules.funsig
+  -> 'a located list
+  -> 'b list * ty
+
+(* -------------------------------------------------------------------- *)
+val trans_args :
+     EcEnv.env
+  -> EcUnify.unienv
+  -> EcLocation.t
+  -> EcModules.funsig
+  -> pexpr list
+  -> expr list * ty
+
 (* -------------------------------------------------------------------- *)
 val trans_restr_for_modty :
   env -> module_type -> pmod_restr option -> mty_mr

tests/eval.ec

@@ -0,0 +1,34 @@
+require import AllCore.
+
+module type I = {
+  proc bar(x : int) : int
+}.
+
+module N : I = {
+  proc bar(x : int) : int = {
+    return 2*x;
+  }
+}.
+
+module M(O : I) = {
+  proc foo(x : int, y : int) : int = {
+    var z, t, u;
+
+    (z, t) <- (2 * x, 3 * y);
+
+    if (x-1 = 1) {
+      y <- y + 1;
+    }
+
+    while (0 < x) {
+      z <- z + 2;
+      x <- x - 1;
+    }
+
+    u <@ O.bar(y);
+
+    return x + y + z * t + u;
+  }
+}.
+
+eval M(N).foo(2, 3).