st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-06-11 03:38:15 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

struct: rev fix, fixes (test is still broken)

Browse source
This commit is contained in:
ProgramSnail 2026-05-10 16:56:15 +00:00
parent 123012f68f
commit 855a3d1ef9
2 changed files with 39 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

65
model_with_structures/analyzer.ml
View file

@ -129,7 +129,7 @@ struct
(* (((snd mem, v) :: fst mem, snd mem + 1), snd mem) *) (* (((snd mem, v) :: fst mem, snd mem + 1), snd mem) *)
(* let mem_set (mem : mem) (id : memid) (v : value) : mem = *) (* let mem_set (mem : mem) (id : memid) (v : value) : mem = *)
(* ((id, v) :: fst mem, snd mem) *) (* ((id, v) :: fst mem, snd mem) *)
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); *) let mem_get (mem : mem) (id : memid) : value = Printf.printf "l%i i%i %i: access\n" (snd mem) id (snd mem - id - 1);
List.nth (fst mem) (snd mem - id - 1) List.nth (fst mem) (snd mem - id - 1)
let mem_add (mem : mem) (v : value) : mem * memid = let mem_add (mem : mem) (v : value) : mem * memid =
((v :: fst mem, snd mem + 1), snd mem) ((v :: fst mem, snd mem + 1), snd mem)
@ -160,7 +160,7 @@ struct
| RefT (_, t) -> t | RefT (_, t) -> t
| _ -> raise @@ Typing_error "pathtype: deref") | _ -> raise @@ Typing_error "pathtype: deref")
| AccessP (p, id) -> match pathtype types p with | AccessP (p, id) -> match pathtype types p with
| TupleT ts -> (List.nth ts id) | TupleT ts -> Printf.printf "pathtype access sz=%i id=%i\n" (List.length ts) id; (List.nth ts id)
| _ -> raise @@ Typing_error "pathtype: access" | _ -> raise @@ Typing_error "pathtype: access"
let rec pathval (mem : mem) (vals : vals) (p : path) : value = match p with let rec pathval (mem : mem) (vals : vals) (p : path) : value = match p with
@ -174,7 +174,7 @@ struct
| RefV id -> mem_get mem id | RefV id -> mem_get mem id
| _ -> raise @@ Typing_error "pathval: deref") | _ -> raise @@ Typing_error "pathval: deref")
| AccessP (p, id) -> match pathval mem vals p with | AccessP (p, id) -> match pathval mem vals p with
| TupleV vs -> (List.nth vs id) | TupleV vs -> Printf.printf "pathval access sz=%i id=%i\n" (List.length vs) id; (List.nth vs id)
| _ -> raise @@ Typing_error "pathval: access" | _ -> raise @@ Typing_error "pathval: access"
(* --- eval rules --- *) (* --- eval rules --- *)
@ -212,7 +212,9 @@ struct
| VarP x, _ -> (mem, b) | VarP x, _ -> (mem, b)
| DerefP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p b in | DerefP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p b in
(mem_set mem' id v', RefV id) (mem_set mem' id v', RefV id)
| AccessP (p, id), TupleV vs -> let (mem', v') = valupd mem (List.nth vs id) p b in | 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')) (mem', TupleV (list_replace vs id v'))
| _, _ -> raise @@ Typing_error "valupd" | _, _ -> raise @@ Typing_error "valupd"
@ -316,7 +318,7 @@ struct
let folder = fun (mem, vs') t u v -> let folder = fun (mem, vs') t u v ->
let (mem', v') = valspoil mem v t u m c in (mem', v' :: vs') in let (mem', v') = valspoil mem v t u m c in (mem', v' :: vs') in
let (mem', vs') = list_foldl3 folder (mem, []) ts us vs in let (mem', vs') = list_foldl3 folder (mem, []) ts us vs in
(mem', TupleV vs') (mem', TupleV (List.rev vs'))
| _, _, _ -> raise @@ Typing_error "valspoil" | _, _, _ -> raise @@ Typing_error "valspoil"
(* full spoil *) (* full spoil *)
@ -328,7 +330,7 @@ struct
let b = pathval mem vals p in (* subvalue in var *) let b = pathval mem vals p in (* subvalue in var *)
let t' = pathtype types p in (* type of subvalue *) let t' = pathtype types p in (* type of subvalue *)
let (mem', b') = valspoil mem b t t' m Cp in (* spoil subvalue *) let (mem', b') = valspoil mem b t t' m Cp in (* spoil subvalue *)
(* TODO: FIXME: why copy (Cp)? *) (* 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 (mem'', v'') = valupd mem' (mem_get mem' id) p b' in (* set subvalue into var *)
mem_set mem'' id v'' mem_set mem'' id v''
@ -401,6 +403,8 @@ struct
let id = vals_assoc x vals in let id = vals_assoc x vals in
let (mem', v') = valupd mem (mem_get mem id) p ZeroV in let (mem', v') = valupd mem (mem_get mem id) p ZeroV in
(mem_set mem' id v', types, vals, visited) (mem_set mem' id v', types, vals, visited)
| RefT _ -> raise @@ Eval_error "write: ref type"
| TupleT _ -> raise @@ Eval_error "write: tuple type"
| _ -> raise @@ Eval_error "write: type") | _ -> raise @@ Eval_error "write: type")
| ReadS p -> if pathval mem vals p == SmthV || pathval mem vals p == BotV | ReadS p -> if pathval mem vals p == SmthV || pathval mem vals p == BotV
then raise @@ Eval_error "read: spoiled value" then raise @@ Eval_error "read: spoiled value"
@ -867,6 +871,8 @@ struct
(* - complex tests *) (* - complex tests *)
(* NOTE: path access isreversed to intuitive function application
by definition *)
let%expect_test "complex test: send, dsl" = let%expect_test "complex test: send, dsl" =
prog_eval_noret ( prog_eval_noret (
(* TODO: set optimal ref mods later *) (* TODO: set optimal ref mods later *)
@ -895,38 +901,38 @@ struct
let sendID = vg9 in let sendID = vg9 in
let send_allID = vg10 in let send_allID = vg10 in
let get_version_idF = FunD ([moded requestT], let get_version_idF = FunD ([moded requestT],
(* (rdS @@ access 1 @@ drf @@ access 0 v0) |. skp) in *) (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in
skp) in (* skp) in *)
(* TODO: real op paths *) (* TODO: real op paths *)
let updated_versionF = FunD ([moded requestT], let updated_versionF = FunD ([moded requestT],
(* (rdS @@ access 2 @@ drf @@ access 0 v0) #. *) (rdS @@ access 0 @@ drf @@ access 2 v0) #.
(* TODO: read all the substructure ?? *) (* TODO: read all the substructure ?? *)
(* (rdS @@ access 1 @@ drf @@ access 0 v0) #. *) (rdS @@ access 0 @@ drf @@ access 1 v0) #.
(* (rdS @@ access 1 @@ drf @@ access 1 v0)) in *) (rdS @@ access 1 @@ drf @@ access 1 v0)) in
skp) in (* skp) in *)
let sendF = FunD ([moded requestT], let sendF = FunD ([moded requestT],
(* (( *) ((
(* (wrS @@ access 2 @@ drf @@ access 0 v0) #. *) (wrS @@ access 0 @@ drf @@ access 2 v0) #.
(* (rdS @@ access 3 @@ drf v0) #. *) (rdS @@ drf @@ access 3 v0) #.
(* (wrS @@ access 3 @@ drf v0) #. *) (* (wrS @@ drf @@ access 3 v0) #. *)
(* (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0) *) (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0)
(* ) |. skp) #. *) ) |. skp) #.
(* (wrS @@ access 4 v0) #. *) (wrS @@ access 4 v0) #.
(* TODO: read all the substructure ?? *) (* TODO: read all the substructure ?? *)
(* (rdS @@ access 4 v0) (*rdS v0*)) in (* FIXME: TMP, parial read, should be full *) *) (rdS @@ access 4 v0) (*rdS v0*)) in (* FIXME: TMP, parial read, should be full *)
skp) in (* skp) in *)
let send_allF = FunD ([moded requestT], let send_allF = FunD ([moded requestT],
(wrS @@ access 4 v0) (*wrS v0*) #. (* FIXME: TMP, parial write, should be full *) (wrS @@ access 4 v0) (*wrS v0*) #. (* FIXME: TMP, parial write, should be full *)
(* (callS sendID [pE v0]) #. *) (callS sendID [pE v0]) #.
(* (callS get_version_idID [pE v0]) #. *) (callS get_version_idID [pE v0]) #.
(* (callS updated_versionID [pE v0]) #. *) (callS updated_versionID [pE v0]) #.
(* TODO: read all the substructure ?? *) (* TODO: read all the substructure ?? *)
(wrS @@ access 1 @@ drf @@ access 0 v0) #. (wrS @@ access 0 @@ drf @@ access 1 v0) #.
(* (wrS @@ access 1 @@ drf @@ access 1 v0) #. *) (wrS @@ access 1 @@ drf @@ access 1 v0) #.
(* --- *) (* --- *)
(* ((rdS @@ access 0 @@ drf @@ access 0 @@ drf @@ access 0 v0) |. *) ((rdS @@ access 0 @@ drf @@ access 0 @@ drf @@ access 0 v0) |.
(* (rdS @@ access 2 @@ drf @@ access 0 v0))) in *) (rdS @@ access 0 @@ drf @@ access 1 v0))) in
skp) in (* skp) in *)
let varID = vg6 in let varID = vg6 in
[ [
defg user_utilsT user_utilsE; defg user_utilsT user_utilsE;
@ -940,7 +946,6 @@ struct
updated_versionF; updated_versionF;
sendF; sendF;
send_allF send_allF
(* TODO: var def *)
], ],
callS send_allID [pE varID] callS send_allID [pE varID]
); );

8
model_with_structures/synthesizer.ml
View file

@ -542,8 +542,7 @@ struct
v == TupleV vs & v == TupleV vs &
tp == TupleT tps & tp == TupleT tps &
list_foldl2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' vs') & list_foldl2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' vs') &
== mem_with_vs' & List.reverso vs' vs'' &
List.reverso vs' vs''
mem_with_id' == Std.pair mem' (TupleV vs'') } mem_with_id' == Std.pair mem' (TupleV vs'') }
} }
@ -791,14 +790,15 @@ struct
valspoilo mem v' tp' u' m ctp' (Std.pair mem_sp v_sp) & valspoilo mem v' tp' u' m ctp' (Std.pair mem_sp v_sp) &
mem_seto mem_sp id' v_sp mem_set & mem_seto mem_sp id' v_sp mem_set &
mem_with_v' == Std.pair mem_set (RefV id') } | mem_with_v' == Std.pair mem_set (RefV id') } |
{ fresh tps, us, vs, mem_sp,vs_sp in { fresh tps, us, vs, mem_sp, vs_sp, vs_sp' in
tp == TupleT tps & tp == TupleT tps &
u == TupleT us & u == TupleT us &
v == TupleV vs & v == TupleV vs &
list_foldl3o (valspoil_foldero m c) list_foldl3o (valspoil_foldero m c)
(Std.pair mem []) tps us vs (Std.pair mem []) tps us vs
(Std.pair mem_sp vs_sp) & (Std.pair mem_sp vs_sp) &
mem_with_v' == Std.pair mem_sp (TupleV vs_sp) List.reverso vs_sp vs_sp' &
mem_with_v' == Std.pair mem_sp (TupleV vs_sp')
} }
} }