Skip to content

Softcode memories in hoare statements #762

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 27 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/ecAst.ml
Original file line number Diff line number Diff line change
Expand Up @@ -231,6 +231,7 @@ and equivS = {
es_po : form; }

and sHoareF = {
hf_m : memory;
hf_pr : form;
hf_f : EcPath.xpath;
hf_po : form;
Expand Down
1 change: 1 addition & 0 deletions src/ecAst.mli
Original file line number Diff line number Diff line change
Expand Up @@ -226,6 +226,7 @@ and equivS = {
es_po : form; }

and sHoareF = {
hf_m : memory;
hf_pr : form;
hf_f : EcPath.xpath;
hf_po : form;
Expand Down
6 changes: 4 additions & 2 deletions src/ecCallbyValue.ml
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ open EcEnv
open EcFol
open EcReduction
open EcBaseLogic
open EcMemory
module BI = EcBigInt

(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -479,11 +480,12 @@ and cbv (st : state) (s : subst) (f : form) (args : args) : form =

| FhoareF hf ->
assert (Args.isempty args);
assert (not (Subst.has_mem s mhr));
assert (not (Subst.has_mem s hf.hf_m));
let hf_pr = norm st s hf.hf_pr in
let hf_po = norm st s hf.hf_po in
let hf_f = norm_xfun st s hf.hf_f in
f_hoareF_r { hf_pr; hf_f; hf_po }
let (hf_m,_) = norm_me s (abstract hf.hf_m) in
f_hoareF_r { hf_m; hf_pr; hf_f; hf_po }

| FhoareS hs ->
assert (Args.isempty args);
Expand Down
4 changes: 2 additions & 2 deletions src/ecCoreFol.ml
Original file line number Diff line number Diff line change
Expand Up @@ -277,8 +277,8 @@ let f_hoareF_r hf = mk_form (FhoareF hf) tbool
let f_hoareS hs_m hs_pr hs_s hs_po =
f_hoareS_r { hs_m; hs_pr; hs_s; hs_po; }

let f_hoareF hf_pr hf_f hf_po =
f_hoareF_r { hf_pr; hf_f; hf_po; }
let f_hoareF hf_m hf_pr hf_f hf_po =
f_hoareF_r { hf_m; hf_pr; hf_f; hf_po; }

(* -------------------------------------------------------------------- *)
let f_eHoareS_r hs = mk_form (FeHoareS hs) tbool
Expand Down
2 changes: 1 addition & 1 deletion src/ecCoreFol.mli
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,7 @@ val f_forall_mems : (EcIdent.t * memtype) list -> form -> form
val f_hoareF_r : sHoareF -> form
val f_hoareS_r : sHoareS -> form

val f_hoareF : form -> xpath -> form -> form
val f_hoareF : memory -> form -> xpath -> form -> form
val f_hoareS : memenv -> form -> stmt -> form -> form

(* soft-constructors - expected hoare *)
Expand Down
3 changes: 1 addition & 2 deletions src/ecCoreSubst.ml
Original file line number Diff line number Diff line change
Expand Up @@ -452,10 +452,9 @@ module Fsubst = struct

| FhoareF hf ->
let hf_f = x_subst s hf.hf_f in
let s = f_rem_mem s mhr in
let hf_pr = f_subst ~tx s hf.hf_pr in
let hf_po = f_subst ~tx s hf.hf_po in
f_hoareF hf_pr hf_f hf_po
f_hoareF hf.hf_m hf_pr hf_f hf_po

| FhoareS hs ->
let hs_s = s_subst s hs.hs_s in
Expand Down
46 changes: 24 additions & 22 deletions src/ecEnv.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1675,15 +1675,16 @@ module Fun = struct
let locals = List.map ovar_of_var fd.f_locals in
(fun_.f_sig,fd), adds_in_memenv mem locals

let inv_memory side =
let id = if side = `Left then EcCoreFol.mleft else EcCoreFol.mright in
EcMemory.abstract id
let inv_memory (side : [`Left | `Right]) =
match side with
| `Left -> EcMemory.abstract EcCoreFol.mleft
| `Right -> EcMemory.abstract EcCoreFol.mright

let inv_memenv env =
Memory.push_all [inv_memory `Left; inv_memory `Rigth] env
let inv_memenv ?(mem = [mleft; mright]) env =
Memory.push_all (List.map EcMemory.abstract mem) env

let inv_memenv1 env =
let mem = EcMemory.abstract EcCoreFol.mhr in
let inv_memenv1 ?(mem = EcCoreFol.mhr) env =
let mem = EcMemory.abstract mem in
Memory.push_active mem env

let prF_memenv m path env =
Expand All @@ -1694,20 +1695,20 @@ module Fun = struct
let post = prF_memenv EcCoreFol.mhr path env in
Memory.push_active post env

let hoareF_memenv path env =
let hoareF_memenv mem path env =
let (ip, _) = oget (ipath_of_xpath path) in
let fun_ = snd (oget (by_ipath ip env)) in
let pre = actmem_pre EcCoreFol.mhr fun_ in
let post = actmem_post EcCoreFol.mhr fun_ in
let pre = actmem_pre mem fun_ in
let post = actmem_post mem fun_ in
pre, post

let hoareF path env =
let pre, post = hoareF_memenv path env in
let hoareF mem path env =
let pre, post = hoareF_memenv mem path env in
Memory.push_active pre env, Memory.push_active post env

let hoareS path env =
let hoareS mem path env =
let fun_ = by_xpath path env in
let fd, memenv = actmem_body EcCoreFol.mhr fun_ in
let fd, memenv = actmem_body mem fun_ in
memenv, fd, Memory.push_active memenv env

let equivF_memenv path1 path2 env =
Expand Down Expand Up @@ -3566,19 +3567,20 @@ module LDecl = struct
let push_all l lenv =
{ lenv with le_env = Memory.push_all l lenv.le_env }

let hoareF xp lenv =
let env1, env2 = Fun.hoareF xp lenv.le_env in
{ lenv with le_env = env1}, {lenv with le_env = env2 }
(* Note: Not confident about this change. I don't understand what this function does *)
let hoareF mem xp lenv =
let env1, env2 = Fun.hoareF mem xp lenv.le_env in
{ lenv with le_env = env1 }, { lenv with le_env = env2 }

let equivF xp1 xp2 lenv =
let env1, env2 = Fun.equivF xp1 xp2 lenv.le_env in
{ lenv with le_env = env1}, {lenv with le_env = env2 }
{ lenv with le_env = env1 }, { lenv with le_env = env2 }

let inv_memenv lenv =
{ lenv with le_env = Fun.inv_memenv lenv.le_env }
let inv_memenv ?mem lenv =
{ lenv with le_env = Fun.inv_memenv ?mem lenv.le_env }

let inv_memenv1 lenv =
{ lenv with le_env = Fun.inv_memenv1 lenv.le_env }
let inv_memenv1 ?mem lenv =
{ lenv with le_env = Fun.inv_memenv1 ?mem lenv.le_env }
end


Expand Down
14 changes: 7 additions & 7 deletions src/ecEnv.mli
Original file line number Diff line number Diff line change
Expand Up @@ -97,18 +97,18 @@ module Fun : sig

val prF : xpath -> env -> env

val hoareF_memenv : xpath -> env -> memenv * memenv
val hoareF_memenv : memory -> xpath -> env -> memenv * memenv

val hoareF : xpath -> env -> env * env
val hoareF : memory -> xpath -> env -> env * env

val hoareS : xpath -> env -> memenv * (funsig * function_def) * env
val hoareS : memory -> xpath -> env -> memenv * (funsig * function_def) * env

val actmem_body : memory -> function_ -> (funsig * function_def) * memenv
val actmem_post : memory -> function_ -> memenv

val inv_memory : [`Left|`Right] -> memenv

val inv_memenv : env -> env
val inv_memenv : ?mem:(memory list) -> env -> env

val equivF_memenv : xpath -> xpath -> env ->
(memenv * memenv) * (memenv * memenv)
Expand Down Expand Up @@ -502,11 +502,11 @@ module LDecl : sig
val push_all : memenv list -> hyps -> hyps
val push_active : memenv -> hyps -> hyps

val hoareF : xpath -> hyps -> hyps * hyps
val hoareF : memory -> xpath -> hyps -> hyps * hyps
val equivF : xpath -> xpath -> hyps -> hyps * hyps

val inv_memenv : hyps -> hyps
val inv_memenv1 : hyps -> hyps
val inv_memenv : ?mem:(memory list) -> hyps -> hyps
val inv_memenv1 : ?mem:memory -> hyps -> hyps
end

val pp_debug_form : (env -> Format.formatter -> form -> unit) ref
2 changes: 1 addition & 1 deletion src/ecHiGoal.ml
Original file line number Diff line number Diff line change
Expand Up @@ -453,8 +453,8 @@ let process_done tc =

(* -------------------------------------------------------------------- *)
let process_apply_bwd ~implicits mode (ff : ppterm) (tc : tcenv1) =
let pt = PT.tc1_process_full_pterm ~implicits tc ff in

let pt = PT.tc1_process_full_pterm ~implicits tc ff in
try
match mode with
| `Alpha ->
Expand Down
16 changes: 11 additions & 5 deletions src/ecLowGoal.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2290,6 +2290,17 @@ type cstate = {
cs_sbeq : Sid.t;
}

let pp_tc1 tc =
pp_tc (FApi.tcenv_of_tcenv1 tc)

let t_debug ?(tag="") t tc =
Format.eprintf "Before (tag: %s):" tag;
pp_tc (FApi.tcenv_of_tcenv1 tc);
let r = t tc in
Format.eprintf "After (tag: %s):" tag;
pp_tc r;
r

let t_crush ?(delta = true) ?tsolve (tc : tcenv1) =

let dtsolve =
Expand All @@ -2299,11 +2310,6 @@ let t_crush ?(delta = true) ?tsolve (tc : tcenv1) =

let tt = FApi.t_try (t_assumption `Alpha) in

(* let t_print s t tc =
Format.eprintf "%s@." s;
pp_tc (FApi.tcenv_of_tcenv1 tc);
t tc in *)

(* Entry of progress: simplify goal, and chain with progress *)
let rec entry (st : cstate) = t_simplify ~delta:`No @! aux0 st

Expand Down
13 changes: 13 additions & 0 deletions src/ecLowGoal.mli
Original file line number Diff line number Diff line change
Expand Up @@ -351,3 +351,16 @@ val t_solve :
-> ?mode:EcMatching.fmoptions
-> ?depth:int
-> FApi.backward

(* -------------------------------------------------------------------- *)
val t_debug :
?tag:string (* for distinguishing prints *)
-> FApi.backward
-> FApi.backward
[@@ocaml.alert debug "Debug function, remove uses before merging"]

val pp_tc :tcenv -> unit
[@@ocaml.alert debug "Debug function, remove uses before merging"]

val pp_tc1 :tcenv1 -> unit
[@@ocaml.alert debug "Debug function, remove uses before merging"]
6 changes: 3 additions & 3 deletions src/ecLowPhlGoal.ml
Original file line number Diff line number Diff line change
Expand Up @@ -254,13 +254,13 @@ let tc1_get_post tc =
(* -------------------------------------------------------------------- *)
let set_pre ~pre f =
match f.f_node with
| FhoareF hf -> f_hoareF pre hf.hf_f hf.hf_po
| FhoareF hf -> f_hoareF_r { hf with hf_pr = pre }
| FhoareS hs -> f_hoareS_r { hs with hs_pr = pre }
| FeHoareF hf -> f_eHoareF_r { hf with ehf_pr = pre }
| FeHoareS hs -> f_eHoareS_r { hs with ehs_pr = pre }
| FbdHoareF hf -> f_bdHoareF pre hf.bhf_f hf.bhf_po hf.bhf_cmp hf.bhf_bd
| FbdHoareF hf -> f_bdHoareF_r { hf with bhf_pr = pre }
| FbdHoareS hs -> f_bdHoareS_r { hs with bhs_pr = pre }
| FequivF ef -> f_equivF pre ef.ef_fl ef.ef_fr ef.ef_po
| FequivF ef -> f_equivF_r { ef with ef_pr = pre }
| FequivS es -> f_equivS_r { es with es_pr = pre }
| _ -> assert false

Expand Down
7 changes: 6 additions & 1 deletion src/ecMatching.ml
Original file line number Diff line number Diff line change
Expand Up @@ -677,7 +677,12 @@ let f_match_core opts hyps (ue, ev) f1 f2 =
| FhoareF hf1, FhoareF hf2 -> begin
if not (EcReduction.EqTest.for_xp env hf1.hf_f hf2.hf_f) then
failure ();
let mxs = Mid.add EcFol.mhr EcFol.mhr mxs in
let subst =
if id_equal hf1.hf_m hf2.hf_m
then subst
else Fsubst.f_bind_mem subst hf1.hf_m hf2.hf_m in
assert (not (Mid.mem hf1.hf_m mxs) && not (Mid.mem hf2.hf_m mxs));
let mxs = Mid.add hf1.hf_m hf2.hf_m mxs in
List.iter2 (doit env (subst, mxs))
[hf1.hf_pr; hf1.hf_po] [hf2.hf_pr; hf2.hf_po]
end
Expand Down
5 changes: 4 additions & 1 deletion src/ecPV.ml
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,10 @@ module PVM = struct
check_binding (fst es.es_ml) s;
check_binding (fst es.es_mr) s;
EcFol.f_map (fun ty -> ty) aux f
| FhoareF _ | FbdHoareF _ ->
| FhoareF hf ->
check_binding hf.hf_m s;
EcFol.f_map (fun ty -> ty) aux f
| FbdHoareF _ ->
check_binding EcFol.mhr s;
EcFol.f_map (fun ty -> ty) aux f
| FhoareS hs ->
Expand Down
26 changes: 14 additions & 12 deletions src/ecPrinting.ml
Original file line number Diff line number Diff line change
Expand Up @@ -787,14 +787,14 @@ let pp_stype (ppe : PPEnv.t) (fmt : Format.formatter) (ty : ty) =
pp_type_r ppe ((1 + fst t_prio_tpl, `NonAssoc), `NonAssoc) fmt ty

(* -------------------------------------------------------------------- *)
let pp_mem (ppe : PPEnv.t) (fmt : Format.formatter) (x : memory) =
let pp_mem (ppe : PPEnv.t) (fmt : Format.formatter) (x as id : memory) =
let x = Format.sprintf "%s" (PPEnv.local_symb ppe x) in
let x =
if x <> "" && x.[0] = '&'
then String.sub x 1 (String.length x - 1)
else x
in
Format.fprintf fmt "%s" x
Format.fprintf fmt "%s<%s>" x (EcIdent.tostring id)

let pp_memtype (ppe : PPEnv.t) (fmt : Format.formatter) (mt : memtype) =
match EcMemory.for_printing mt with
Expand Down Expand Up @@ -1811,7 +1811,7 @@ and pp_form_core_r
Format.fprintf fmt "%a{%s%a}"
(pp_pv ppe) x (if force then "!" else "") (pp_mem ppe) i in

let force =
let force = true ||
match x with
| PVloc x -> Ssym.mem x ppe.ppe_inuse
| PVglob _ -> false in
Expand Down Expand Up @@ -1886,23 +1886,25 @@ and pp_form_core_r
end

| FhoareF hf ->
let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.hf_f ppe.PPEnv.ppe_env in
let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.hf_m hf.hf_f ppe.PPEnv.ppe_env in
let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in
let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in
Format.fprintf fmt "hoare[@[<hov 2>@ %a :@ @[%a ==>@ %a@]@]]"
Format.fprintf fmt "hoare[@[<hov 2>@ %a {%a} :@ @[%a ==>@ %a@]@]]"
(pp_funname ppe) hf.hf_f
(pp_mem ppe) hf.hf_m
(pp_form ppepr) hf.hf_pr
(pp_form ppepo) hf.hf_po

| FhoareS hs ->
let ppe = PPEnv.push_mem ppe ~active:true hs.hs_m in
Format.fprintf fmt "hoare[@[<hov 2>@ %a :@ @[%a ==>@ %a@]@]]"
Format.fprintf fmt "hoare[@[<hov 2>@ %a {%a} :@ @[%a ==>@ %a@]@]]"
(pp_stmt_for_form ppe) hs.hs_s
(pp_mem ppe) (fst hs.hs_m)
(pp_form ppe) hs.hs_pr
(pp_form ppe) hs.hs_po

| FeHoareF hf ->
let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.ehf_f ppe.PPEnv.ppe_env in
let mepr, mepo = EcEnv.Fun.hoareF_memenv mhr hf.ehf_f ppe.PPEnv.ppe_env in
let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in
let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in
Format.fprintf fmt
Expand Down Expand Up @@ -1954,7 +1956,7 @@ and pp_form_core_r
(pp_form ppepo) eg.eg_po

| FbdHoareF hf ->
let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.bhf_f ppe.PPEnv.ppe_env in
let mepr, mepo = EcEnv.Fun.hoareF_memenv mhr hf.bhf_f ppe.PPEnv.ppe_env in
let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in
let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in
Format.fprintf fmt "phoare[@[<hov 2>@ %a :@ @[%a ==>@ %a@]@]] %s %a"
Expand Down Expand Up @@ -2903,12 +2905,12 @@ let pp_post (ppe : PPEnv.t) ?prpo fmt post =

(* -------------------------------------------------------------------- *)
let pp_hoareF (ppe : PPEnv.t) ?prpo fmt hf =
let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.hf_f ppe.PPEnv.ppe_env in
let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.hf_m hf.hf_f ppe.PPEnv.ppe_env in
let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in
let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in

Format.fprintf fmt "%a@\n%!" (pp_pre ppepr ?prpo) hf.hf_pr;
Format.fprintf fmt " %a@\n%!" (pp_funname ppe) hf.hf_f;
Format.fprintf fmt " %a {%a}@\n%!" (pp_funname ppe) hf.hf_f (pp_mem ppe) hf.hf_m;
Format.fprintf fmt "@\n%a%!" (pp_post ppepo ?prpo) hf.hf_po

(* -------------------------------------------------------------------- *)
Expand All @@ -2928,7 +2930,7 @@ let pp_hoareS (ppe : PPEnv.t) ?prpo fmt hs =

(* -------------------------------------------------------------------- *)
let pp_eHoareF (ppe : PPEnv.t) ?prpo fmt hf =
let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.ehf_f ppe.PPEnv.ppe_env in
let mepr, mepo = EcEnv.Fun.hoareF_memenv mhr hf.ehf_f ppe.PPEnv.ppe_env in
let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in
let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in

Expand Down Expand Up @@ -2960,7 +2962,7 @@ let string_of_hrcmp = function

(* -------------------------------------------------------------------- *)
let pp_bdhoareF (ppe : PPEnv.t) ?prpo fmt hf =
let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.bhf_f ppe.PPEnv.ppe_env in
let mepr, mepo = EcEnv.Fun.hoareF_memenv mhr hf.bhf_f ppe.PPEnv.ppe_env in
let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in
let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in

Expand Down
5 changes: 4 additions & 1 deletion src/ecReduction.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1453,7 +1453,10 @@ let rec conv ri env f1 f2 stk =
conv_next ri env f1 stk

| FhoareF hf1, FhoareF hf2 when EqTest_i.for_xp env hf1.hf_f hf2.hf_f ->
conv ri env hf1.hf_pr hf2.hf_pr (zhl f1 [hf1.hf_po] [hf2.hf_po] stk)
let subst = if id_equal hf1.hf_m hf2.hf_m then Fsubst.f_subst_id
else Fsubst.f_bind_mem Fsubst.f_subst_id hf1.hf_m hf2.hf_m in
let subst = Fsubst.f_subst subst in
conv ri env hf1.hf_pr (subst hf2.hf_pr) (zhl f1 [hf1.hf_po] [subst hf2.hf_po] stk)

| FhoareS hs1, FhoareS hs2
when EqTest_i.for_stmt env hs1.hs_s hs2.hs_s ->
Expand Down
Loading
Loading