mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-06-11 03:38:15 +00:00
struct: reverse paths in valupd (fix): update for analyzer and synthesizer
This commit is contained in:
ProgramSnail
parent
62e6a55810
commit
e8e6acc122
2 changed files with 67 additions and 34 deletions
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue