Skip to content

Commit c063e99

Browse files
oskgostrub
oskgo
authored and
strub
committed
expose memory binding in program logic statements to user
1 parent 23cf445 commit c063e99

File tree

4 files changed

+103
-110
lines changed

4 files changed

+103
-110
lines changed

‎src/ecParser.mly‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1124,10 +1124,10 @@ sform_u(P):
11241124
| EAGER LBRACKET eb=eager_body(P) RBRACKET { eb }
11251125

11261126
| PR LBRACKET
1127-
mp=loc(fident) args=paren(plist0(form_r(P), COMMA)) AT pn=mident
1127+
mp=loc(fident) args=paren(plist0(form_r(P), COMMA)) m=brace(mident)? AT pn=mident
11281128
COLON event=form_r(P)
11291129
RBRACKET
1130-
{ PFprob (mp, args, pn, event) }
1130+
{ PFprob (m, mp, args, pn, event) }
11311131

11321132
| r=loc(RBOOL)
11331133
{ PFident (mk_loc r.pl_loc EcCoreLib.s_dbool, None) }
@@ -1222,30 +1222,30 @@ hoare_bd_cmp :
12221222
| GE { EcAst.FHge }
12231223

12241224
hoare_body(P):
1225-
mp=loc(fident) COLON pre=form_r(P) LONGARROW post=form_r(P)
1226-
{ PFhoareF (pre, mp, post) }
1225+
mp=loc(fident) m=brace(mident)? COLON pre=form_r(P) LONGARROW post=form_r(P)
1226+
{ PFhoareF (m, pre, mp, post) }
12271227

12281228
ehoare_body(P):
1229-
mp=loc(fident) COLON pre=form_r(P) LONGARROW
1229+
mp=loc(fident) m=brace(mident)? COLON pre=form_r(P) LONGARROW
12301230
post=form_r(P)
1231-
{ PFehoareF (pre, mp, post) }
1231+
{ PFehoareF (m, pre, mp, post) }
12321232

12331233
phoare_body(P):
1234-
LBRACKET mp=loc(fident) COLON
1234+
LBRACKET mp=loc(fident) m=brace(mident)? COLON
12351235
pre=form_r(P) LONGARROW post=form_r(P)
12361236
RBRACKET
12371237
cmp=hoare_bd_cmp bd=sform_r(P)
1238-
{ PFBDhoareF (pre, mp, post, cmp, bd) }
1238+
{ PFBDhoareF (m, pre, mp, post, cmp, bd) }
12391239

12401240
equiv_body(P):
1241-
mp1=loc(fident) TILD mp2=loc(fident)
1241+
mp1=loc(fident) ml=brace(mident)? TILD mp2=loc(fident) mr=brace(mident)?
12421242
COLON pre=form_r(P) LONGARROW post=form_r(P)
1243-
{ PFequivF (pre, (mp1, mp2), post) }
1243+
{ PFequivF (ml, mr, pre, (mp1, mp2), post) }
12441244

12451245
eager_body(P):
1246-
| s1=stmt COMMA mp1=loc(fident) TILD mp2=loc(fident) COMMA s2=stmt
1246+
| s1=stmt COMMA mp1=loc(fident) ml=brace(mident)? TILD mp2=loc(fident) COMMA s2=stmt mr=brace(mident)?
12471247
COLON pre=form_r(P) LONGARROW post=form_r(P)
1248-
{ PFeagerF (pre, (s1, mp1, mp2,s2), post) }
1248+
{ PFeagerF (ml, mr, pre, (s1, mp1, mp2,s2), post) }
12491249

12501250
pgtybinding1:
12511251
| x=ptybinding1

‎src/ecParsetree.ml‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -202,12 +202,12 @@ and pformula_r =
202202
| PFlsless of pgamepath
203203
| PFscope of pqsymbol * pformula
204204

205-
| PFhoareF of pformula * pgamepath * pformula
206-
| PFehoareF of pformula * pgamepath * pformula
207-
| PFequivF of pformula * (pgamepath * pgamepath) * pformula
208-
| PFeagerF of pformula * (pstmt * pgamepath * pgamepath * pstmt) * pformula
209-
| PFprob of pgamepath * (pformula list) * pmemory * pformula
210-
| PFBDhoareF of pformula * pgamepath * pformula * phoarecmp * pformula
205+
| PFhoareF of psymbol option * pformula * pgamepath * pformula
206+
| PFehoareF of psymbol option * pformula * pgamepath * pformula
207+
| PFequivF of psymbol option * psymbol option * pformula * (pgamepath * pgamepath) * pformula
208+
| PFeagerF of psymbol option * psymbol option * pformula * (pstmt * pgamepath * pgamepath * pstmt) * pformula
209+
| PFprob of psymbol option * pgamepath * (pformula list) * pmemory * pformula
210+
| PFBDhoareF of psymbol option * pformula * pgamepath * pformula * phoarecmp * pformula
211211

212212
and pmemtype_el = ([`Single|`Tuple] * (psymbol list)) located * pty
213213
and pmemtype = pmemtype_el list

‎src/ecPrinting.ml‎

Lines changed: 63 additions & 77 deletions
Original file line numberDiff line numberDiff line change
@@ -840,6 +840,10 @@ let pp_mem (ppe : PPEnv.t) (fmt : Format.formatter) (x as id : memory) =
840840
else
841841
Format.fprintf fmt "%s" x
842842

843+
let pp_pl_mem_binding b ppe fmt m =
844+
if b then
845+
Format.fprintf fmt "{&%a}" (pp_mem ppe) m
846+
843847
let pp_memtype (ppe : PPEnv.t) (fmt : Format.formatter) (mt : memtype) =
844848
match EcMemory.for_printing mt with
845849
| None -> Format.fprintf fmt "{}"
@@ -1936,46 +1940,40 @@ and pp_form_core_r
19361940
let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.hf_m hf.hf_f ppe.PPEnv.ppe_env in
19371941
let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in
19381942
let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in
1939-
if debug_mode then
1940-
Format.fprintf fmt "hoare[@[<hov 2>@ %a {%a} :@ @[%a ==>@ %a@]@]]"
1941-
(pp_funname ppe) hf.hf_f
1942-
(pp_mem ppe) hf.hf_m
1943-
(pp_form ppepr) (hf_pr hf).inv
1944-
(pp_form ppepo) (hf_po hf).inv
1945-
else
1946-
Format.fprintf fmt "hoare[@[<hov 2>@ %a :@ @[%a ==>@ %a@]@]]"
1947-
(pp_funname ppe) hf.hf_f
1948-
(pp_form ppepr) (hf_pr hf).inv
1949-
(pp_form ppepo) (hf_po hf).inv
1943+
let pm = debug_mode || hf.hf_m.id_symb <> "&hr" in
1944+
Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@]@]]"
1945+
(pp_funname ppe) hf.hf_f
1946+
(pp_pl_mem_binding pm ppe) hf.hf_m
1947+
(pp_form ppepr) (hf_pr hf).inv
1948+
(pp_form ppepo) (hf_po hf).inv
19501949

19511950
| FhoareS hs ->
19521951
let ppe = PPEnv.push_mem ppe ~active:true hs.hs_m in
1953-
if debug_mode then
1954-
Format.fprintf fmt "hoare[@[<hov 2>@ %a {%a} :@ @[%a ==>@ %a@]@]]"
1952+
let pm = debug_mode || (fst hs.hs_m).id_symb <> "&hr" in
1953+
Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@]@]]"
19551954
(pp_stmt_for_form ppe) hs.hs_s
1956-
(pp_mem ppe) (fst hs.hs_m)
1955+
(pp_pl_mem_binding pm ppe) (fst hs.hs_m)
19571956
(pp_form ppe) (hs_pr hs).inv
19581957
(pp_form ppe) (hs_po hs).inv
1959-
else
1960-
Format.fprintf fmt "hoare[@[<hov 2>@ %a :@ @[%a ==>@ %a@]@]]"
1961-
(pp_stmt_for_form ppe) hs.hs_s
1962-
(pp_form ppe) (hs_pr hs).inv
1963-
(pp_form ppe) (hs_po hs).inv
1964-
1958+
19651959
| FeHoareF hf ->
19661960
let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.ehf_m hf.ehf_f ppe.PPEnv.ppe_env in
19671961
let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in
19681962
let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in
1963+
let pm = debug_mode || hf.ehf_m.id_symb <> "&hr" in
19691964
Format.fprintf fmt
1970-
"ehoare[@[<hov 2>@ %a :@ @[%a ==>@ %a@]@]]"
1965+
"ehoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@]@]]"
19711966
(pp_funname ppe) hf.ehf_f
1967+
(pp_pl_mem_binding pm ppe) hf.ehf_m
19721968
(pp_form ppepr) (ehf_pr hf).inv
19731969
(pp_form ppepo) (ehf_po hf).inv
19741970

19751971
| FeHoareS hs ->
19761972
let ppe = PPEnv.push_mem ppe ~active:true hs.ehs_m in
1977-
Format.fprintf fmt "ehoare[@[<hov 2>@ %a :@ @[%a ==>@ %a@]@]]"
1973+
let pm = debug_mode || (fst hs.ehs_m).id_symb <> "&hr" in
1974+
Format.fprintf fmt "ehoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@]@]]"
19781975
(pp_stmt_for_form ppe) hs.ehs_s
1976+
(pp_pl_mem_binding pm ppe) (fst hs.ehs_m)
19791977
(pp_form ppe) (ehs_pr hs).inv
19801978
(pp_form ppe) (ehs_po hs).inv
19811979

@@ -1984,28 +1982,27 @@ and pp_form_core_r
19841982
EcEnv.Fun.equivF_memenv eqv.ef_ml eqv.ef_mr eqv.ef_fl eqv.ef_fr ppe.PPEnv.ppe_env in
19851983
let ppepr = PPEnv.create_and_push_mems ppe [meprl; meprr] in
19861984
let ppepo = PPEnv.create_and_push_mems ppe [mepol; mepor] in
1987-
if debug_mode then
1988-
Format.fprintf fmt "equiv[@[<hov 2>@ %a {%a} ~@ %a {%a} :@ @[%a ==>@ %a@]@]]"
1985+
let pml = eqv.ef_ml.id_symb <> "&1" || debug_mode in
1986+
let pmr = eqv.ef_mr.id_symb <> "&2" || debug_mode in
1987+
Format.fprintf fmt "equiv[@[<hov 2>@ %a %a ~@ %a %a:@ @[%a ==>@ %a@]@]]"
19891988
(pp_funname ppe) eqv.ef_fl
1990-
(pp_mem ppe) eqv.ef_ml
1989+
(pp_pl_mem_binding pml ppe) eqv.ef_ml
19911990
(pp_funname ppe) eqv.ef_fr
1992-
(pp_mem ppe) eqv.ef_mr
1991+
(pp_pl_mem_binding pmr ppe) eqv.ef_mr
19931992
(pp_form ppepr) (ef_pr eqv).inv
19941993
(pp_form ppepo) (ef_po eqv).inv
1995-
else
1996-
Format.fprintf fmt "equiv[@[<hov 2>@ %a ~@ %a :@ @[%a ==>@ %a@]@]]"
1997-
(pp_funname ppe) eqv.ef_fl
1998-
(pp_funname ppe) eqv.ef_fr
1999-
(pp_form ppepr) (ef_pr eqv).inv
2000-
(pp_form ppepo) (ef_po eqv).inv
20011994

20021995
| FequivS es ->
20031996
let ppef = PPEnv.push_mems ppe [es.es_ml; es.es_mr] in
20041997
let ppel = PPEnv.push_mem ppe ~active:true es.es_ml in
20051998
let pper = PPEnv.push_mem ppe ~active:true es.es_mr in
2006-
Format.fprintf fmt "equiv[@[<hov 2>@ %a ~@ %a :@ @[%a ==>@ %a@]@]]"
1999+
let pml = (fst es.es_ml).id_symb <> "&1" || debug_mode in
2000+
let pmr = (fst es.es_mr).id_symb <> "&2" || debug_mode in
2001+
Format.fprintf fmt "equiv[@[<hov 2>@ %a %a ~@ %a %a:@ @[%a ==>@ %a@]@]]"
20072002
(pp_stmt_for_form ppel) es.es_sl
2003+
(pp_pl_mem_binding pml ppe) (fst es.es_ml)
20082004
(pp_stmt_for_form pper) es.es_sr
2005+
(pp_pl_mem_binding pmr ppe) (fst es.es_mr)
20092006
(pp_form ppef) (es_pr es).inv
20102007
(pp_form ppef) (es_po es).inv
20112008

@@ -2014,48 +2011,47 @@ and pp_form_core_r
20142011
EcEnv.Fun.equivF_memenv eg.eg_ml eg.eg_mr eg.eg_fl eg.eg_fr ppe.PPEnv.ppe_env in
20152012
let ppepr = PPEnv.create_and_push_mems ppe [meprl; meprr] in
20162013
let ppepo = PPEnv.create_and_push_mems ppe [mepol; mepor] in
2017-
Format.fprintf fmt "eager[@[<hov 2>@ %a,@ %a ~@ %a,@ %a :@ @[%a ==>@ %a@]@]]"
2014+
let pml = eg.eg_ml.id_symb <> "&1" || debug_mode in
2015+
let pmr = eg.eg_mr.id_symb <> "&2" || debug_mode in
2016+
Format.fprintf fmt "eager[@[<hov 2>@ %a,@ %a %a~@ %a,@ %a %a:@ @[%a ==>@ %a@]@]]"
20182017
(pp_stmt_for_form ppe) eg.eg_sl
20192018
(pp_funname ppe) eg.eg_fl
2019+
(pp_pl_mem_binding pml ppe) eg.eg_ml
20202020
(pp_funname ppe) eg.eg_fr
20212021
(pp_stmt_for_form ppe) eg.eg_sr
2022+
(pp_pl_mem_binding pmr ppe) eg.eg_mr
20222023
(pp_form ppepr) (eg_pr eg).inv
20232024
(pp_form ppepo) (eg_po eg).inv
20242025

20252026
| FbdHoareF hf ->
20262027
let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.bhf_m hf.bhf_f ppe.PPEnv.ppe_env in
20272028
let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in
20282029
let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in
2029-
if debug_mode then
2030-
Format.fprintf fmt "phoare[@[<hov 2>@ %a {%a} :@ @[%a ==>@ %a@]@]] %s %a"
2031-
(pp_funname ppe) hf.bhf_f
2032-
(pp_mem ppe) hf.bhf_m
2033-
(pp_form ppepr) (bhf_pr hf).inv
2034-
(pp_form ppepo) (bhf_po hf).inv
2035-
(string_of_hcmp hf.bhf_cmp)
2036-
(pp_form_r ppepr (max_op_prec,`NonAssoc)) (bhf_bd hf).inv
2037-
else
2038-
Format.fprintf fmt "phoare[@[<hov 2>@ %a :@ @[%a ==>@ %a@]@]] %s %a"
2039-
(pp_funname ppe) hf.bhf_f
2040-
(pp_form ppepr) (bhf_pr hf).inv
2041-
(pp_form ppepo) (bhf_po hf).inv
2042-
(string_of_hcmp hf.bhf_cmp)
2043-
(pp_form_r ppepr (max_op_prec,`NonAssoc)) (bhf_bd hf).inv
2030+
let pm = debug_mode || hf.bhf_m.id_symb <> "&hr" in
2031+
Format.fprintf fmt "phoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@]@]] %s %a"
2032+
(pp_funname ppe) hf.bhf_f
2033+
(pp_pl_mem_binding pm ppe) hf.bhf_m
2034+
(pp_form ppepr) (bhf_pr hf).inv
2035+
(pp_form ppepo) (bhf_po hf).inv
2036+
(string_of_hcmp hf.bhf_cmp)
2037+
(pp_form_r ppepr (max_op_prec,`NonAssoc)) (bhf_bd hf).inv
20442038

20452039
| FbdHoareS hs ->
20462040
let ppef = PPEnv.push_mem ppe ~active:true hs.bhs_m in
2047-
Format.fprintf fmt "phoare[@[<hov 2>@ %a :@ @[%a ==>@ %a@]@]] %s %a"
2041+
let pm = debug_mode || (fst hs.bhs_m).id_symb <> "&hr" in
2042+
Format.fprintf fmt "phoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@]@]] %s %a"
20482043
(pp_stmt_for_form ppef) hs.bhs_s
2044+
(pp_pl_mem_binding pm ppe) (fst hs.bhs_m)
20492045
(pp_form ppef) (bhs_pr hs).inv
20502046
(pp_form ppef) (bhs_po hs).inv
20512047
(string_of_hcmp hs.bhs_cmp)
20522048
(pp_form_r ppef (max_op_prec,`NonAssoc)) (bhs_bd hs).inv
20532049

20542050
| Fpr pr->
20552051
let me = EcEnv.Fun.prF_memenv pr.pr_event.m pr.pr_fun ppe.PPEnv.ppe_env in
2056-
20572052
let ppep = PPEnv.create_and_push_mem ppe ~active:true me in
2058-
Format.fprintf fmt "Pr[@[%a@[%t@] @@ %a :@ %a@]]"
2053+
let pm = debug_mode || pr.pr_event.m.id_symb <> "&hr" in
2054+
Format.fprintf fmt "Pr[@[%a@[%t@] %a@@ %a :@ %a@]]"
20592055
(pp_funname ppe) pr.pr_fun
20602056
(match pr.pr_args.f_node with
20612057
| Ftuple _ ->
@@ -2064,6 +2060,7 @@ and pp_form_core_r
20642060
(fun fmt -> pp_string fmt "()")
20652061
| _ ->
20662062
(fun fmt -> Format.fprintf fmt "(%a)" (pp_form ppe) pr.pr_args))
2063+
(pp_pl_mem_binding pm ppe) pr.pr_event.m
20672064
(pp_local ppe) pr.pr_mem
20682065
(pp_form ppep) pr.pr_event.inv
20692066

@@ -2987,10 +2984,8 @@ let pp_hoareF (ppe : PPEnv.t) ?prpo fmt hf =
29872984
let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in
29882985

29892986
Format.fprintf fmt "%a@\n%!" (pp_pre ppepr ?prpo) (hf_pr hf).inv;
2990-
if debug_mode then
2991-
Format.fprintf fmt " %a {%a}@\n%!" (pp_funname ppe) hf.hf_f (pp_mem ppe) hf.hf_m
2992-
else
2993-
Format.fprintf fmt " %a@\n%!" (pp_funname ppe) hf.hf_f;
2987+
let pm = debug_mode || hf.hf_m.id_symb <> "&hr" in
2988+
Format.fprintf fmt " %a %a@\n%!" (pp_funname ppe) hf.hf_f (pp_pl_mem_binding pm ppe) hf.hf_m;
29942989
Format.fprintf fmt "@\n%a%!" (pp_post ppepo ?prpo) (hf_po hf).inv
29952990

29962991
(* -------------------------------------------------------------------- *)
@@ -3016,10 +3011,8 @@ let pp_eHoareF (ppe : PPEnv.t) ?prpo fmt hf =
30163011
let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in
30173012

30183013
Format.fprintf fmt "%a@\n%!" (pp_pre ppepr ?prpo) (ehf_pr hf).inv;
3019-
if debug_mode then
3020-
Format.fprintf fmt " %a {%a}@\n%!" (pp_funname ppe) hf.ehf_f (pp_mem ppe) hf.ehf_m
3021-
else
3022-
Format.fprintf fmt " %a@\n%!" (pp_funname ppe) hf.ehf_f;
3014+
let pm = debug_mode || hf.ehf_m.id_symb <> "&hr" in
3015+
Format.fprintf fmt " %a %a@\n%!" (pp_funname ppe) hf.ehf_f (pp_pl_mem_binding pm ppe) hf.ehf_m;
30233016
Format.fprintf fmt "@\n%a%!" (pp_post ppepo ?prpo) (ehf_po hf).inv
30243017

30253018
(* -------------------------------------------------------------------- *)
@@ -3054,10 +3047,8 @@ let pp_bdhoareF (ppe : PPEnv.t) ?prpo fmt hf =
30543047
let scmp = string_of_hrcmp hf.bhf_cmp in
30553048

30563049
Format.fprintf fmt "%a@\n%!" (pp_pre ppepr ?prpo) (bhf_pr hf).inv;
3057-
if debug_mode then
3058-
Format.fprintf fmt " %a {%a}@\n%!" (pp_funname ppe) hf.bhf_f (pp_mem ppe) hf.bhf_m
3059-
else
3060-
Format.fprintf fmt " %a@\n%!" (pp_funname ppe) hf.bhf_f;
3050+
let pm = debug_mode || hf.bhf_m.id_symb <> "&hr" in
3051+
Format.fprintf fmt " %a %a@\n%!" (pp_funname ppe) hf.bhf_f (pp_pl_mem_binding pm ppe) hf.bhf_m;
30613052
Format.fprintf fmt " %s @[<hov 2>%a@]@\n%!" scmp (pp_form ppepr) (bhf_bd hf).inv;
30623053
Format.fprintf fmt "@\n%a%!" (pp_post ppepo ?prpo) (bhf_po hf).inv
30633054

@@ -3086,19 +3077,14 @@ let pp_equivF (ppe : PPEnv.t) ?prpo fmt ef =
30863077
let ppepr = PPEnv.create_and_push_mems ppe [meprl; meprr] in
30873078
let ppepo = PPEnv.create_and_push_mems ppe [mepol; mepor] in
30883079
Format.fprintf fmt "%a@\n%!" (pp_pre ppepr ?prpo) (ef_pr ef).inv;
3089-
if debug_mode then begin
3090-
Format.fprintf fmt " %a {%a} ~ %a {%a}@\n%!"
3091-
(pp_funname ppe) ef.ef_fl
3092-
(pp_mem ppe) ef.ef_ml
3093-
(pp_funname ppe) ef.ef_fr
3094-
(pp_mem ppe) ef.ef_mr;
3095-
Format.fprintf fmt "@\n%a%!" (pp_post ppepo ?prpo) (ef_po ef).inv;
3096-
end else begin
3097-
Format.fprintf fmt " %a ~ %a@\n%!"
3098-
(pp_funname ppe) ef.ef_fl
3099-
(pp_funname ppe) ef.ef_fr;
3100-
Format.fprintf fmt "@\n%a%!" (pp_post ppepo ?prpo) (ef_po ef).inv
3101-
end
3080+
let pml = debug_mode || ef.ef_ml.id_symb <> "&1" in
3081+
let pmr = debug_mode || ef.ef_mr.id_symb <> "&2" in
3082+
Format.fprintf fmt " %a %a~ %a %a@\n%!"
3083+
(pp_funname ppe) ef.ef_fl
3084+
(pp_pl_mem_binding pml ppe) ef.ef_ml
3085+
(pp_funname ppe) ef.ef_fr
3086+
(pp_pl_mem_binding pmr ppe) ef.ef_mr;
3087+
Format.fprintf fmt "@\n%a%!" (pp_post ppepo ?prpo) (ef_po ef).inv
31023088

31033089
(* -------------------------------------------------------------------- *)
31043090
let pp_equivS (ppe : PPEnv.t) ?prpo fmt es =

0 commit comments

Comments
 (0)