From e8e6acc12244c3cce7a5234cee1563c57ec2cabc Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 10 May 2026 17:19:00 +0000 Subject: [PATCH] struct: reverse paths in valupd (fix): update for analyzer and synthesizer --- model_with_structures/analyzer.ml | 44 +++++++++++---------- model_with_structures/synthesizer.ml | 57 ++++++++++++++++++++-------- 2 files changed, 67 insertions(+), 34 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 77dd0f9..a38bda1 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -73,6 +73,8 @@ struct | RefV of memid | TupleV of value list + type revpath = VarRP | DerefRP of revpath | AccessRP of revpath * data + (* TODO: any additional difference between rvalue and lvalue now ?? *) (* --- *) @@ -129,7 +131,7 @@ struct (* (((snd mem, v) :: fst mem, snd mem + 1), snd mem) *) (* let mem_set (mem : mem) (id : memid) (v : value) : mem = *) (* ((id, v) :: fst mem, snd mem) *) - let mem_get (mem : mem) (id : memid) : value = Printf.printf "l%i i%i %i: access\n" (snd mem) id (snd mem - id - 1); + let mem_get (mem : mem) (id : memid) : value = (* FIXME TMP Printf.printf "l%i i%i %i: access\n" (snd mem) id (snd mem - id - 1); *) List.nth (fst mem) (snd mem - id - 1) let mem_add (mem : mem) (v : value) : mem * memid = ((v :: fst mem, snd mem + 1), snd mem) @@ -154,13 +156,19 @@ struct | DerefP p -> pathvar p | AccessP (p, _) -> pathvar p + let rec pathrev (p : path) (acc : revpath) : revpath = match p with + | VarP x -> acc + | DerefP p -> pathrev p @@ DerefRP acc + | AccessP (p, i) -> pathrev p @@ AccessRP (acc, i) + let rec pathtype (types : types) (p : path) : atype = match p with | VarP x -> types_assoc x types | DerefP p -> (match pathtype types p with | RefT (_, t) -> t | _ -> raise @@ Typing_error "pathtype: deref") | AccessP (p, id) -> match pathtype types p with - | TupleT ts -> Printf.printf "pathtype access sz=%i id=%i\n" (List.length ts) id; (List.nth ts id) + | TupleT ts -> (* FIXME TMP Printf.printf "pathtype access sz=%i id=%i\n" (List.length ts) id; *) + (List.nth ts id) | _ -> raise @@ Typing_error "pathtype: access" let rec pathval (mem : mem) (vals : vals) (p : path) : value = match p with @@ -174,7 +182,8 @@ struct | RefV id -> mem_get mem id | _ -> raise @@ Typing_error "pathval: deref") | AccessP (p, id) -> match pathval mem vals p with - | TupleV vs -> Printf.printf "pathval access sz=%i id=%i\n" (List.length vs) id; (List.nth vs id) + | TupleV vs -> (* FIXME TMP Printf.printf "pathval access sz=%i id=%i\n" (List.length vs) id; *) + (List.nth vs id) | _ -> raise @@ Typing_error "pathval: access" (* --- eval rules --- *) @@ -208,14 +217,14 @@ struct (* - value update *) - let rec valupd (mem : mem) (v : value) (p : path) (b : value) : mem * value = match p, v with - | VarP x, _ -> (mem, b) - | DerefP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p b in - (mem_set mem' id v', RefV id) - | AccessP (p, id), TupleV vs -> let (mem', v') = (* FIXME TMP Printf.printf "vs size=%i id=%i\n" (List.length vs) id; *) - valupd mem (List.nth vs id) p b in - (* FIXME TMP Printf.printf "before return\n"; *) - (mem', TupleV (list_replace vs id v')) + let rec valupd (mem : mem) (v : value) (p : revpath) (b : value) : mem * value = match p, v with + | VarRP, _ -> (mem, b) + | DerefRP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p b in + (mem_set mem' id v', RefV id) + | AccessRP (p, id), TupleV vs -> let (mem', v') = (* FIXME TMP Printf.printf "vs size=%i id=%i\n" (List.length vs) id; *) + valupd mem (List.nth vs id) p b in + (* FIXME TMP Printf.printf "before return\n"; *) + (mem', TupleV (list_replace vs id v')) | _, _ -> raise @@ Typing_error "valupd" (* - value combination *) @@ -331,7 +340,8 @@ struct let t' = pathtype types p in (* type of subvalue *) let (mem', b') = valspoil mem b t t' m Cp in (* spoil subvalue *) (* TODO: FIXME: why copy (Cp)? maybe sometimes use top-level capability ? *) - let (mem'', v'') = valupd mem' (mem_get mem' id) p b' in (* set subvalue into var *) + let pi = pathrev p VarRP in + let (mem'', v'') = valupd mem' (mem_get mem' id) pi b' in (* set subvalue into var *) mem_set mem'' id v'' let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem = @@ -401,7 +411,8 @@ struct then raise @@ Eval_error "write: write tag" else let x = pathvar p in let id = vals_assoc x vals in - let (mem', v') = valupd mem (mem_get mem id) p ZeroV in + let pi = pathrev p VarRP in + let (mem', v') = valupd mem (mem_get mem id) pi ZeroV in (mem_set mem' id v', types, vals, visited) | RefT _ -> raise @@ Eval_error "write: ref type" | TupleT _ -> raise @@ Eval_error "write: tuple type" @@ -902,25 +913,21 @@ struct let send_allID = vg10 in let get_version_idF = FunD ([moded requestT], (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in - (* skp) in *) - (* TODO: real op paths *) let updated_versionF = FunD ([moded requestT], (rdS @@ access 0 @@ drf @@ access 2 v0) #. (* TODO: read all the substructure ?? *) (rdS @@ access 0 @@ drf @@ access 1 v0) #. (rdS @@ access 1 @@ drf @@ access 1 v0)) in - (* skp) in *) let sendF = FunD ([moded requestT], (( (wrS @@ access 0 @@ drf @@ access 2 v0) #. (rdS @@ drf @@ access 3 v0) #. - (* (wrS @@ drf @@ access 3 v0) #. *) + (wrS @@ drf @@ access 3 v0) #. (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0) ) |. skp) #. (wrS @@ access 4 v0) #. (* TODO: read all the substructure ?? *) (rdS @@ access 4 v0) (*rdS v0*)) in (* FIXME: TMP, parial read, should be full *) - (* skp) in *) let send_allF = FunD ([moded requestT], (wrS @@ access 4 v0) (*wrS v0*) #. (* FIXME: TMP, parial write, should be full *) (callS sendID [pE v0]) #. @@ -932,7 +939,6 @@ struct (* --- *) ((rdS @@ access 0 @@ drf @@ access 0 @@ drf @@ access 0 v0) |. (rdS @@ access 0 @@ drf @@ access 1 v0))) in - (* skp) in *) let varID = vg6 in [ defg user_utilsT user_utilsE; diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index f3c1dd7..99de175 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -105,7 +105,6 @@ struct (* end *) end - (* TODO: access: data or int ? *) module Path = struct [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [%%ocanren_inject @@ -174,6 +173,15 @@ struct ] end + module RevPath = struct + [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] + [%%ocanren_inject + type nonrec ('d, 'p) t = VarRP | DerefRP of 'p | AccessRP of 'p * 'd + [@@deriving gt ~options:{ show; gmap }] + type ground = (Nat.ground, ground) t + ] + end + (* --- *) module MemEnv = struct @@ -462,6 +470,21 @@ struct { fresh p', _id in p == AccessP (p', _id) & pathvaro p' x } } + let rec pathrevo p rp rp' = + let open Path in + let open RevPath in + ocanren { + { fresh _x in + p == VarP _x & + rp == rp' } | + { fresh p' in + p == DerefP p' & + pathrevo p' (DerefRP rp) rp' } | + { fresh p', id in + p == AccessP (p', id) & + pathrevo p' (AccessRP (rp, id)) rp' } + } + let rec pathtypeo types p tp = let open Path in let open Type in @@ -548,26 +571,26 @@ struct (* - value update *) - let rec valupdo mem v p b mem_with_v' = - let open Path in + (* NOTE: reversed path used *) + let rec valupdo mem v rp b mem_with_v' = + let open RevPath in let open Value in ocanren { - { fresh x in - p == VarP x & + { rp == VarRP & mem_with_v' == Std.pair mem b } | - { fresh p', id, v', mem_upd, v_upd, mem_with_v_upd, mem_st in - p == DerefP p' & + { fresh rp', id, v', mem_upd, v_upd, mem_with_v_upd, mem_st in + rp == DerefRP rp' & v == RefV id & mem_geto mem id v' & - valupdo mem v' p' b mem_with_v_upd & + valupdo mem v' rp' b mem_with_v_upd & Std.pair mem_upd v_upd == mem_with_v_upd & mem_seto mem_upd id v_upd mem_st & mem_with_v' == Std.pair mem_st (RefV id) } | - { fresh p', id, vs', v', mem_upd, v_upd, mem_with_v_upd, vs_upd in - p == AccessP (p', id) & + { fresh rp', id, vs', v', mem_upd, v_upd, mem_with_v_upd, vs_upd in + rp == AccessRP (rp', id) & v == TupleV vs' & list_ntho vs' id v' & - valupdo mem v' p' b mem_with_v_upd & + valupdo mem v' rp' b mem_with_v_upd & Std.pair mem_upd v_upd == mem_with_v_upd & list_replaceo vs' id v_upd vs_upd & mem_with_v' == Std.pair mem_upd (TupleV vs_upd) } @@ -807,9 +830,10 @@ struct let argspoilpo st m tp p mem' = let open StEnv in let open CopyCap in + let open RevPath in ocanren { fresh mem, types, vals, visited, - x, id, b, tp', + x, id, b, tp', rp, mem_sp, b_sp, v_sp, mem_upd, v_upd in st == StEnv (mem, types, vals, visited) & pathvaro p x & @@ -818,7 +842,8 @@ struct pathtypeo types p tp' & valspoilo mem b tp tp' m Cp (Std.pair mem_sp b_sp) & mem_geto mem_sp id v_sp & - valupdo mem_sp v_sp p b_sp (Std.pair mem_upd v_upd) & + pathrevo p VarRP rp & + valupdo mem_sp v_sp rp b_sp (Std.pair mem_upd v_upd) & mem_seto mem_upd id v_upd mem' } @@ -914,6 +939,7 @@ struct let open WriteCap in let open TypesEnv in let open ValsEnv in + let open RevPath in ocanren { fresh mem, types, vals, visited in st == StEnv (mem, types, vals, visited) & @@ -949,7 +975,7 @@ struct mem tps es mem_spoiled & st' == StEnv (mem_spoiled, types, vals, visited') } | - { fresh p, tp, _r, w, x, id, v, + { fresh p, tp, _r, w, x, id, v, rp, mem_upd, v_upd, mem_set in s == WriteS p & pathtypeo types p tp & @@ -958,7 +984,8 @@ struct pathvaro p x & vals_assoco x vals id & mem_geto mem id v & - valupdo mem v p ZeroV (Std.pair mem_upd v_upd) & + pathrevo p VarRP rp & + valupdo mem v rp ZeroV (Std.pair mem_upd v_upd) & mem_seto mem_upd id v_upd mem_set & st' == StEnv (mem_set, types, vals, visited) } | { fresh p in