Skip to content

Commit f685e10

Browse files
strubstrub
committed
New vernacular command: eval
Target: evaluation of pWhile programs.
1 parent 1393a49 commit f685e10

File tree

8 files changed

+221
-0
lines changed

8 files changed

+221
-0
lines changed

‎src/ecCommands.ml

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -747,6 +747,37 @@ and process_dump scope (source, tc) =
747747

748748
scope
749749

750+
(* -------------------------------------------------------------------- *)
751+
and process_eval (scope : EcScope.scope) ((f, args) : pgamepath * pexpr list) =
752+
let env = EcScope.env scope in
753+
let fpath = EcTyping.trans_gamepath env f in
754+
let fun_ = EcEnv.Fun.by_xpath fpath env in
755+
let args =
756+
let ue = EcUnify.UniEnv.create None in
757+
let args, _ = EcTyping.trans_args env ue f.pl_loc fun_.f_sig args in
758+
if not (EcUnify.UniEnv.closed ue) then
759+
EcScope.hierror "cannot infer all type variables";
760+
let subst = EcUnify.UniEnv.close ue in
761+
let subst = EcCoreSubst.Tuni.subst subst in
762+
let args = List.map (EcCoreSubst.e_subst subst) args in
763+
args
764+
in
765+
766+
let aout = EcProcEval.eval env (fpath, args) in
767+
768+
begin
769+
match aout with
770+
| None ->
771+
EcScope.notify scope `Warning
772+
"%s" "cannot compute a concrete value"
773+
774+
| Some aout ->
775+
let ppe = EcPrinting.PPEnv.ofenv env in
776+
EcScope.notify scope `Info "%a" (EcPrinting.pp_expr ppe) aout
777+
end;
778+
779+
scope
780+
750781
(* -------------------------------------------------------------------- *)
751782
and process (ld : Loader.loader) (scope : EcScope.scope) g =
752783
let loc = g.pl_loc in
@@ -791,6 +822,7 @@ and process (ld : Loader.loader) (scope : EcScope.scope) g =
791822
| Greduction red -> `Fct (fun scope -> process_reduction scope red)
792823
| Ghint hint -> `Fct (fun scope -> process_hint scope hint)
793824
| GdumpWhy3 file -> `Fct (fun scope -> process_dump_why3 scope file)
825+
| Geval call -> `Fct (fun scope -> process_eval scope call)
794826
with
795827
| `Fct f -> Some (f scope)
796828
| `State f -> f scope; None

‎src/ecLexer.mll

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -214,6 +214,7 @@
214214
"dump" , DUMP ; (* KW: global *)
215215
"remove" , REMOVE ; (* KW: global *)
216216
"exit" , EXIT ; (* KW: global *)
217+
"eval" , EVAL ; (* KW: global *)
217218

218219
"fail" , FAIL ; (* KW: internal *)
219220
"time" , TIME ; (* KW: internal *)

‎src/ecParser.mly

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -422,6 +422,7 @@
422422
%token EQ
423423
%token EQUIV
424424
%token ETA
425+
%token EVAL
425426
%token EXACT
426427
%token EXFALSO
427428
%token EXIST
@@ -3793,6 +3794,12 @@ user_red_option:
37933794
(* Search pattern *)
37943795
%inline search: x=sform_h { x }
37953796

3797+
(* -------------------------------------------------------------------- *)
3798+
(* Evaluation *)
3799+
eval:
3800+
| EVAL mp=loc(fident) args=paren(plist0(expr, COMMA))
3801+
{ (mp, args) }
3802+
37963803
(* -------------------------------------------------------------------- *)
37973804
(* Global entries *)
37983805

@@ -3832,6 +3839,7 @@ global_action:
38323839
| SEARCH x=search+ { Gsearch x }
38333840
| LOCATE x=qident { Glocate x }
38343841
| WHY3 x=STRING { GdumpWhy3 x }
3842+
| eval { Geval $1 }
38353843

38363844
| PRAGMA x=pragma { Gpragma x }
38373845
| PRAGMA PLUS x=pragma { Goption (x, `Bool true ) }

‎src/ecParsetree.ml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1301,6 +1301,7 @@ type global_action =
13011301
| Gpragma of psymbol
13021302
| Goption of (psymbol * [`Bool of bool | `Int of int])
13031303
| GdumpWhy3 of string
1304+
| Geval of (pgamepath * pexpr list)
13041305

13051306
type global = {
13061307
gl_action : global_action located;

‎src/ecProcEval.ml

Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,120 @@
1+
(* -------------------------------------------------------------------- *)
2+
open EcUtils
3+
open EcPath
4+
open EcAst
5+
6+
(* -------------------------------------------------------------------- *)
7+
let eval (env : EcEnv.env) =
8+
let exception NotAValue in
9+
10+
let hyps = EcEnv.LDecl.init env [] in
11+
let cbv = EcCallbyValue.norm_cbv EcReduction.full_red hyps in
12+
13+
let rec get_function (fpath : xpath) =
14+
let fun_ = EcEnv.Fun.by_xpath fpath env in
15+
16+
match fun_.f_def with
17+
| FBdef def -> fun_, def
18+
| FBalias alias -> let _, def = get_function alias in fun_, def
19+
| _ -> raise NotAValue in
20+
21+
let rec is_literal (f : form) =
22+
match EcFol.sform_of_form f with
23+
| SFtrue | SFfalse | SFint _ -> true
24+
| SFtuple fs -> List.for_all is_literal fs
25+
| _ -> false in
26+
27+
let eval (subst : EcPV.PVM.subst) (v : form) =
28+
let aout = cbv (EcPV.PVM.subst env subst v) in
29+
if not (is_literal aout) then raise NotAValue;
30+
aout in
31+
32+
let rec doit (fpath : xpath) (args : form list) =
33+
let fun_, body = get_function fpath in
34+
let subst =
35+
List.fold_left2 (fun (subst : EcPV.PVM.subst) (var : ovariable) (arg : form) ->
36+
var.ov_name |> Option.fold ~none:subst ~some:(fun name ->
37+
let pv = EcTypes.pv_loc name in
38+
EcPV.PVM.add env pv mhr arg subst
39+
)
40+
) EcPV.PVM.empty fun_.f_sig.fs_anames args in
41+
42+
let subst = for_stmt subst body.f_body in
43+
44+
Option.map
45+
(eval subst -| EcFol.form_of_expr mhr)
46+
body.f_ret
47+
48+
and for_instr (subst : EcPV.PVM.subst) (instr : EcModules.instr) =
49+
match instr.i_node with
50+
| Sasgn (lvalue, rvalue) -> begin
51+
let rvalue = eval subst (EcFol.form_of_expr mhr rvalue) in
52+
match lvalue with
53+
| LvVar (pv, _) ->
54+
EcPV.PVM.add env pv mhr rvalue subst
55+
| LvTuple pvs ->
56+
let rvalue = EcFol.destr_tuple rvalue in
57+
List.fold_left2 (fun subst (pv, _) rvalue ->
58+
EcPV.PVM.add env pv mhr rvalue subst
59+
) subst pvs rvalue
60+
end
61+
62+
| Scall (lv, f, args) -> begin
63+
let args = List.map (eval subst -| EcFol.form_of_expr mhr) args in
64+
let aout = doit f args in
65+
66+
match lv with
67+
| None ->
68+
subst
69+
70+
| Some (LvVar (pv, _)) ->
71+
EcPV.PVM.add env pv mhr (Option.get aout) subst
72+
73+
| Some (LvTuple pvs) ->
74+
List.fold_left2 (fun subst (pv, _) aout ->
75+
EcPV.PVM.add env pv mhr aout subst
76+
) subst pvs (EcFol.destr_tuple (Option.get aout))
77+
end
78+
79+
| Sif (cond, strue, sfalse) ->
80+
let cond = eval subst (EcFol.form_of_expr mhr cond) in
81+
let branch =
82+
match EcFol.sform_of_form cond with
83+
| SFtrue -> strue
84+
| SFfalse -> sfalse
85+
| _ -> raise NotAValue in
86+
87+
for_stmt subst branch
88+
89+
| Swhile (cond, body) -> begin
90+
let cond = eval subst (EcFol.form_of_expr mhr cond) in
91+
92+
match EcFol.sform_of_form cond with
93+
| SFtrue ->
94+
let subst = for_stmt subst body in
95+
let subst = for_instr subst instr in
96+
subst
97+
98+
| SFfalse ->
99+
subst
100+
101+
| _ ->
102+
raise NotAValue
103+
end
104+
105+
| Sabstract _
106+
| Sassert _
107+
| Smatch _
108+
| Srnd _ -> raise NotAValue
109+
110+
and for_stmt (subst : EcPV.PVM.subst) (stmt : stmt) =
111+
List.fold_left for_instr subst stmt.s_node
112+
113+
in
114+
115+
fun ((fpath, args) : xpath * expr list) ->
116+
try
117+
let aout =
118+
doit fpath (List.map (cbv -| EcFol.form_of_expr mhr) args)
119+
in Option.map (EcFol.expr_of_form mhr) aout
120+
with NotAValue -> None

‎src/ecProcEval.mli

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
(* -------------------------------------------------------------------- *)
2+
open EcPath
3+
open EcAst
4+
5+
(* -------------------------------------------------------------------- *)
6+
val eval : EcEnv.env -> xpath * expr list -> expr option

‎src/ecTyping.mli

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -256,6 +256,25 @@ val trans_pattern : env -> ptnmap -> EcUnify.unienv -> pformula -> EcFol.form
256256
val trans_memtype :
257257
env -> EcUnify.unienv -> pmemtype -> EcMemory.memtype
258258

259+
(* -------------------------------------------------------------------- *)
260+
val transcall :
261+
('a located -> 'b * ty)
262+
-> EcEnv.env
263+
-> EcUnify.unienv
264+
-> EcLocation.t
265+
-> EcModules.funsig
266+
-> 'a located list
267+
-> 'b list * ty
268+
269+
(* -------------------------------------------------------------------- *)
270+
val trans_args :
271+
EcEnv.env
272+
-> EcUnify.unienv
273+
-> EcLocation.t
274+
-> EcModules.funsig
275+
-> pexpr list
276+
-> expr list * ty
277+
259278
(* -------------------------------------------------------------------- *)
260279
val trans_restr_for_modty :
261280
env -> module_type -> pmod_restr option -> mty_mr

‎tests/eval.ec

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
require import AllCore.
2+
3+
module type I = {
4+
proc bar(x : int) : int
5+
}.
6+
7+
module N : I = {
8+
proc bar(x : int) : int = {
9+
return 2*x;
10+
}
11+
}.
12+
13+
module M(O : I) = {
14+
proc foo(x : int, y : int) : int = {
15+
var z, t, u;
16+
17+
(z, t) <- (2 * x, 3 * y);
18+
19+
if (x-1 = 1) {
20+
y <- y + 1;
21+
}
22+
23+
while (0 < x) {
24+
z <- z + 2;
25+
x <- x - 1;
26+
}
27+
28+
u <@ O.bar(y);
29+
30+
return x + y + z * t + u;
31+
}
32+
}.
33+
34+
eval M(N).foo(2, 3).

0 commit comments

Comments
 (0)