mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-06-11 03:38:15 +00:00
Compare commits
No commits in common. "441b3837622e279b1963d06c39837650b0f3f98f" and "d06f6d53bc99994a516f50774a83c952fea32a6e" have entirely different histories.
441b383762
...
d06f6d53bc
4 changed files with 353 additions and 387 deletions
|
|
@ -14,7 +14,7 @@ struct
|
|||
type in_cap = In | NIn
|
||||
type out_cap = Out | NOut
|
||||
|
||||
type mode = Mode of in_cap * out_cap
|
||||
type mode = in_cap * out_cap
|
||||
|
||||
type path = VarP of data | DerefP of path | AccessP of path * data
|
||||
|
||||
|
|
@ -103,12 +103,10 @@ struct
|
|||
|
||||
let types_add (types : types) (x : data) (t : atype) =
|
||||
(x, t) :: types
|
||||
|
||||
let vals_add (vals : vals) (x : data) (id : memid) =
|
||||
(x, id) :: vals
|
||||
|
||||
let mode_in (m : mode) : in_cap = match m with Mode (i, _) -> i
|
||||
let mode_out (m : mode) : out_cap = match m with Mode (_, o) -> o
|
||||
|
||||
(* - utils *)
|
||||
|
||||
let rec list_replace (xs : 'a list) (id : int) (y : 'a) : 'a list = match xs, id with
|
||||
|
|
@ -351,9 +349,9 @@ struct
|
|||
(* TODO: check assignment type matches types separately later ?? *)
|
||||
let is_correct_tags (r : read_cap) (w : write_cap)
|
||||
(m : mode) (c : copy_cap) : bool =
|
||||
(mode_out m != Out || c == Rf) &&
|
||||
(mode_out m != Out || w == AlwaysWr) &&
|
||||
(r != Rd || mode_in m == In)
|
||||
(snd m != Out || c == Rf) &&
|
||||
(snd m != Out || w == AlwaysWr) &&
|
||||
(r != Rd || fst m == In)
|
||||
|
||||
let tryread (r : read_cap) (v_m : memval)
|
||||
(v_r : readval) (v_w : writeval) : value =
|
||||
|
|
@ -365,10 +363,10 @@ struct
|
|||
|
||||
let tryspoil (m : mode) (w : write_cap) (v_m : memval) : memval =
|
||||
match m, w with
|
||||
| Mode (_, Out), AlwaysWr -> v_m
|
||||
| Mode (_, Out), MayWr -> v_m
|
||||
| Mode (_, NOut), AlwaysWr -> BotMV
|
||||
| Mode (_, NOut), MayWr -> SmthMV
|
||||
| (_, Out), AlwaysWr -> v_m
|
||||
| (_, Out), MayWr -> v_m
|
||||
| (_, NOut), AlwaysWr -> BotMV
|
||||
| (_, NOut), MayWr -> SmthMV
|
||||
| _ -> raise @@ Typing_error "tryspoil: unexpected pair mode + write cap"
|
||||
|
||||
let rec valspoil (mem : mem) (v : value) (t : atype)
|
||||
|
|
@ -609,7 +607,7 @@ struct
|
|||
let rfT t = RefT (Rf, t)
|
||||
let cpT t = RefT (Cp, t)
|
||||
|
||||
let moded t = (Mode (In, NOut), t)
|
||||
let moded t = ((In, NOut), t)
|
||||
|
||||
let defg t = VarD t
|
||||
|
||||
|
|
@ -870,7 +868,7 @@ struct
|
|||
wrS @@ drf @@ v0
|
||||
);
|
||||
FunD (
|
||||
[(Mode (In, Out), rfT @@ uT_aw)],
|
||||
[((In, Out), rfT @@ uT_aw)],
|
||||
wrS @@ drf @@ v0
|
||||
)
|
||||
],
|
||||
|
|
@ -932,10 +930,10 @@ struct
|
|||
defg (rfT uT_r_aw);
|
||||
FunD (
|
||||
[
|
||||
(Mode (NIn, NOut), cpT @@ uT);
|
||||
(Mode (In, NOut), cpT @@ uT_r_aw);
|
||||
(Mode (NIn, Out), rfT @@ uT_aw);
|
||||
(Mode (In, Out), rfT @@ uT_r_aw);
|
||||
((NIn, NOut), cpT @@ uT);
|
||||
((In, NOut), cpT @@ uT_r_aw);
|
||||
((NIn, Out), rfT @@ uT_aw);
|
||||
((In, Out), rfT @@ uT_r_aw);
|
||||
],
|
||||
(rdS @@ drf @@ v1) #.
|
||||
(rdS @@ drf @@ v3) #.
|
||||
|
|
@ -966,10 +964,10 @@ struct
|
|||
defg (rfT uT_r_aw);
|
||||
FunD (
|
||||
[
|
||||
(Mode (NIn, NOut), rfT @@ uT);
|
||||
(Mode (In, NOut), rfT @@ uT_r);
|
||||
(Mode (NIn, Out), rfT @@ uT_aw);
|
||||
(Mode (In, Out), rfT @@ uT_r_aw);
|
||||
((NIn, NOut), rfT @@ uT);
|
||||
((In, NOut), rfT @@ uT_r);
|
||||
((NIn, Out), rfT @@ uT_aw);
|
||||
((In, Out), rfT @@ uT_r_aw);
|
||||
],
|
||||
(rdS @@ drf @@ v1) #.
|
||||
(rdS @@ drf @@ v3) #.
|
||||
|
|
@ -1051,4 +1049,130 @@ struct
|
|||
);
|
||||
Printf.printf "done!";
|
||||
[%expect {| done! |}]
|
||||
|
||||
(* TODO tags, access *)
|
||||
(* let%expect_test "presentation test 2 (complex types), dsl" = *)
|
||||
(* prog_eval_noret ( *)
|
||||
(* let userT = TupleT [uT_r_aw; uT_r_aw; uT_r_aw] in *)
|
||||
(* let dataT = TupleT [uT_r_aw; uT_r_aw] in *)
|
||||
(* let requestT = TupleT [cpT userT; *)
|
||||
(* cpT dataT; *)
|
||||
(* cpT dataT] in *)
|
||||
(* let requestArgsT = TupleT [cpT userT; (* TODO: tags *) *)
|
||||
(* cpT dataT; *)
|
||||
(* cpT dataT] in *)
|
||||
(* let userE = TupleE [UnitE; UnitE; UnitE] in *)
|
||||
(* let dataE = TupleE [UnitE; UnitE] in *)
|
||||
(* let requestE = TupleE [rfg0E; rfg1E; rfg2E] in *)
|
||||
(* [ *)
|
||||
(* defg userT userE; *)
|
||||
(* defg dataT dataE; *)
|
||||
(* defg uT_r_aw; (* time *) *)
|
||||
(* defg requestT requestE; *)
|
||||
(* FunD ( (* send *) *)
|
||||
(* [ *)
|
||||
(* (moded @@ requestArgsT) *)
|
||||
(* ], *)
|
||||
(* ( *)
|
||||
(* ( (* TODO access *) *)
|
||||
(* (rdS @@ drf @@ v0) #. *)
|
||||
(* (wrS @@ drf @@ v0) #. *)
|
||||
(* (rdS @@ drf @@ v0) #. *)
|
||||
(* (wrS @@ drf @@ v0) *)
|
||||
(* ) |. *)
|
||||
(* skp) #. *)
|
||||
(* TODO access *)
|
||||
(* (wrS @@ drf @@ v0) #. *)
|
||||
(* (rdS @@ drf @@ v1) *)
|
||||
(* ); *)
|
||||
(* ], *)
|
||||
(* (callS vg4 [pE vg3]) #. *)
|
||||
(* TODO access *)
|
||||
(* (wrS @@ drf @@ vg3) #. *)
|
||||
(* ((rdS @@ drf @@ vg3) |. (rdS @@ drf @@ vg3)) #. *)
|
||||
(* (rdS @@ drf @@ vg3) *)
|
||||
(* ); *)
|
||||
(* Printf.printf "done!"; *)
|
||||
(* [%expect {| done! |}] *)
|
||||
|
||||
(* - complex tests *)
|
||||
|
||||
(* TODO: FIXME: rw tags *)
|
||||
(* NOTE: path access isreversed to intuitive function application
|
||||
by definition *)
|
||||
(* let%expect_test "complex test: send, dsl" = *)
|
||||
(* prog_eval_noret ( *)
|
||||
(* TODO: set optimal ref mods later *)
|
||||
(* let user_utilsT = TupleT [uT_r_aw (* 0 id *); uT_r_aw] in *)
|
||||
(* let user_infoT = TupleT [uT_r_aw (* 0 name *); uT_r_aw; uT_r_aw] in *)
|
||||
(* let userT = TupleT [cpT user_utilsT (* 0 utils *); cpT user_infoT (* 1 info *)] in *)
|
||||
(* let versionT = TupleT [uT_r_aw (* 0 id *); uT_r_aw; uT_r_aw] in *)
|
||||
(* let utilsT = TupleT [uT_r_aw (* 0 has_version *); uT_r_aw (* 1 id *)] in *)
|
||||
(* let requestT = TupleT [cpT userT (* 0 user *); *)
|
||||
(* cpT versionT (* 1 version *); *)
|
||||
(* cpT utilsT (* 2 utils *); *)
|
||||
(* cpT uT_r_aw (* 3 data *); *)
|
||||
(* uT_r_aw (* 4 operation_date *)] in *)
|
||||
(* let user_utilsE = TupleE [UnitE (* 0 id *); UnitE] in *)
|
||||
(* let user_infoE = TupleE [UnitE (* 0 name *); UnitE; UnitE] in *)
|
||||
(* let userE = TupleE [rfg0E (* 0 utils *); rfg1E (* 1 info *)] in *)
|
||||
(* let versionE = TupleE [UnitE (* 0 id *); UnitE; UnitE] in *)
|
||||
(* let utilsE = TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] in *)
|
||||
(* let requestE = TupleE [rfg2E (* 0 user *); *)
|
||||
(* rfg3E (* 1 version *); *)
|
||||
(* rfg4E (* 2 utils *); *)
|
||||
(* rfg5E (* 3 data *); *)
|
||||
(* UnitE (* 4 operation_date *)] in *)
|
||||
(* let get_version_idID = vg7 in *)
|
||||
(* let updated_versionID = vg8 in *)
|
||||
(* let sendID = vg9 in *)
|
||||
(* let send_allID = vg10 in *)
|
||||
(* let get_version_idF = FunD ([moded requestT], *)
|
||||
(* (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in *)
|
||||
(* 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 *)
|
||||
(* let sendF = FunD ([moded requestT], *)
|
||||
(* (( *)
|
||||
(* (wrS @@ access 0 @@ drf @@ access 2 v0) #. *)
|
||||
(* (rdS @@ 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 *) *)
|
||||
(* let send_allF = FunD ([moded requestT], *)
|
||||
(* (wrS @@ access 4 v0) (*wrS v0*) #. (* FIXME: TMP, parial write, should be full *) *)
|
||||
(* (callS sendID [pE v0]) #. *)
|
||||
(* (callS get_version_idID [pE v0]) #. *)
|
||||
(* (callS updated_versionID [pE v0]) #. *)
|
||||
(* TODO: read all the substructure ?? *)
|
||||
(* (wrS @@ access 0 @@ 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 1 v0))) in *)
|
||||
(* let varID = vg6 in *)
|
||||
(* [ *)
|
||||
(* defg user_utilsT user_utilsE; *)
|
||||
(* defg user_infoT user_infoE; *)
|
||||
(* defg userT userE; *)
|
||||
(* defg versionT versionE; *)
|
||||
(* defg utilsT utilsE; *)
|
||||
(* defg uT_r_aw; *)
|
||||
(* defg requestT requestE; *)
|
||||
(* get_version_idF; *)
|
||||
(* updated_versionF; *)
|
||||
(* sendF; *)
|
||||
(* send_allF *)
|
||||
(* ], *)
|
||||
(* callS send_allID [pE varID] *)
|
||||
(* ); *)
|
||||
(* Printf.printf "done!"; *)
|
||||
(* [%expect {| done! |}] *)
|
||||
|
||||
(* TODO: version with more optimal modifiers *)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -1,48 +1,35 @@
|
|||
module FunctionalRW =
|
||||
module Functional =
|
||||
struct
|
||||
open GT
|
||||
|
||||
type data = int
|
||||
[@@deriving gt ~options:{ show }]
|
||||
type memid = int
|
||||
[@@deriving gt ~options:{ show }]
|
||||
|
||||
(* --- syntax --- *)
|
||||
|
||||
type read_cap = Rd | NRd | UndefRd
|
||||
[@@deriving gt ~options:{ show }]
|
||||
type read_cap = Rd | NRd (* | UndefRd ? *)
|
||||
|
||||
type write_cap = AlwaysWr | MayWr | NeverWr | UndefWr
|
||||
[@@deriving gt ~options:{ show }]
|
||||
type copy_cap = Rf | Cp
|
||||
[@@deriving gt ~options:{ show }]
|
||||
type write_cap = AlwaysWr | MayWr | NeverWr (* | UndefWr ? *)
|
||||
type copy_cap = Cp | Rf
|
||||
|
||||
type in_cap = In | NIn
|
||||
[@@deriving gt ~options:{ show }]
|
||||
type out_cap = Out | NOut
|
||||
[@@deriving gt ~options:{ show }]
|
||||
|
||||
type mode = Mode of in_cap * out_cap
|
||||
[@@deriving gt ~options:{ show }]
|
||||
type mode = in_cap * out_cap
|
||||
|
||||
type path = VarP of data | DerefP of path | AccessP of path * data
|
||||
[@@deriving gt ~options:{ show }]
|
||||
|
||||
type atype = UnitT of read_cap * write_cap
|
||||
| RefT of copy_cap * atype
|
||||
| TupleT of atype list
|
||||
| FunT of (mode * atype) list (* TODO: declaration id for ease of impl / performance instead (?) *)
|
||||
[@@deriving gt ~options:{ show }]
|
||||
|
||||
type mtype = mode * atype
|
||||
[@@deriving gt ~options:{ show }]
|
||||
|
||||
type expr = UnitE
|
||||
| PathE of path
|
||||
(* TODO: extend to include arbitrary path *)
|
||||
| RefE of data
|
||||
| TupleE of expr list
|
||||
[@@deriving gt ~options:{ show }]
|
||||
|
||||
type stmt = SkipS
|
||||
| CallS of path * expr list
|
||||
|
|
@ -50,14 +37,11 @@ struct
|
|||
| ReadS of path
|
||||
| SeqS of stmt * stmt
|
||||
| ChoiceS of stmt * stmt
|
||||
[@@deriving gt ~options:{ show }]
|
||||
|
||||
type decl = VarD of (* data * *) atype (* * expr *)
|
||||
| FunD of (* data * *) (* (data * *) mtype (* ) *) list * stmt
|
||||
[@@deriving gt ~options:{ show }]
|
||||
|
||||
type prog = decl list * stmt
|
||||
[@@deriving gt ~options:{ show }]
|
||||
|
||||
(* --- exceptions --- *)
|
||||
|
||||
|
|
@ -72,7 +56,6 @@ struct
|
|||
exception Typing_error of string
|
||||
exception Eval_error of string
|
||||
exception Cant_fold3_error
|
||||
exception Cant_deduce_rw_error of string
|
||||
|
||||
(* value model & memory model *)
|
||||
|
||||
|
|
@ -84,36 +67,26 @@ struct
|
|||
(* | TupleDV of deepvalue list *)
|
||||
|
||||
type memval = ZeroMV | SmthMV | BotMV (* | TopMV ?? *)
|
||||
[@@deriving gt ~options:{ show }]
|
||||
type readval = ZeroRV | OneRV | TopRV
|
||||
[@@deriving gt ~options:{ show }]
|
||||
type writeval = ZeroWV | SmthWV | OneWV
|
||||
[@@deriving gt ~options:{ show }]
|
||||
|
||||
type value = UnitV of memval * readval * writeval
|
||||
| FunV (* of ((* data list * *) stmt) list *)
|
||||
| RefV of memid
|
||||
| TupleV of value list
|
||||
[@@deriving gt ~options:{ show }]
|
||||
|
||||
type revpath = VarRP | DerefRP of revpath | AccessRP of revpath * data
|
||||
[@@deriving gt ~options:{ show }]
|
||||
|
||||
type action = ReadA | AlwaysWriteA | MayWriteA
|
||||
[@@deriving gt ~options:{ show }]
|
||||
|
||||
(* TODO: any additional difference between rvalue and lvalue now ?? *)
|
||||
|
||||
(* --- *)
|
||||
|
||||
type mem = value list * memid (* NOTE: memory and first free elem *)
|
||||
[@@deriving gt ~options:{ show }]
|
||||
type types = (data * atype) list
|
||||
[@@deriving gt ~options:{ show }]
|
||||
type vals = (data * memid) list
|
||||
[@@deriving gt ~options:{ show }]
|
||||
type state = mem * types * vals
|
||||
[@@deriving gt ~options:{ show }]
|
||||
|
||||
(* --- *)
|
||||
|
||||
|
|
@ -130,12 +103,10 @@ struct
|
|||
|
||||
let types_add (types : types) (x : data) (t : atype) =
|
||||
(x, t) :: types
|
||||
|
||||
let vals_add (vals : vals) (x : data) (id : memid) =
|
||||
(x, id) :: vals
|
||||
|
||||
let mode_in (m : mode) : in_cap = match m with Mode (i, _) -> i
|
||||
let mode_out (m : mode) : out_cap = match m with Mode (_, o) -> o
|
||||
|
||||
(* - utils *)
|
||||
|
||||
let rec list_replace (xs : 'a list) (id : int) (y : 'a) : 'a list = match xs, id with
|
||||
|
|
@ -221,8 +192,6 @@ struct
|
|||
match t with
|
||||
| UnitT (Rd, _) -> (mem, UnitV (ZeroMV, ZeroRV, ZeroWV))
|
||||
| UnitT (NRd, _) -> (mem, UnitV (BotMV, ZeroRV, ZeroWV))
|
||||
(* NOTE: ignore pre-tag in rw-analysis *)
|
||||
| UnitT (UndefRd, _) -> (mem, UnitV (ZeroMV, ZeroRV, ZeroWV))
|
||||
| FunT _ -> raise @@ Typing_error "valbuild: funciton value is not supported"
|
||||
| RefT (_, t) -> let (mem', v') = valbuild mem t in
|
||||
let (mem'', id'') = mem_add mem' v' in
|
||||
|
|
@ -232,6 +201,22 @@ struct
|
|||
let mem', vs' = List.fold_right folder ts (mem, []) in
|
||||
(mem', TupleV vs')
|
||||
|
||||
(* NOTE: not needed now *)
|
||||
(* let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = *)
|
||||
(* match t, v with *)
|
||||
(* | UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV)) *)
|
||||
(* | UnitT (NRd, _), UnitV _ -> (mem, UnitV (BotMV, ZeroRV, ZeroWV)) *)
|
||||
(* | FunT _, FunV -> (mem, v) *)
|
||||
(* | RefT (Rf, _), RefV _ -> (mem, v) *)
|
||||
(* | RefT (_, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in *)
|
||||
(* let (mem'', id'') = mem_add mem' v' in *)
|
||||
(* (mem'', RefV id'') *)
|
||||
(* | TupleT ts, TupleV vs -> let folder = fun v t (mem, vs') -> let (mem', v') = valcopy mem v t in *)
|
||||
(* (mem', v' :: vs') in *)
|
||||
(* let mem', vs' = List.fold_right2 folder vs ts (mem, []) in *)
|
||||
(* (mem', TupleV vs') *)
|
||||
(* | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type" *)
|
||||
|
||||
(* - action rules *)
|
||||
|
||||
let memvmod (a : action) (v_m : memval) : memval =
|
||||
|
|
@ -353,14 +338,20 @@ struct
|
|||
(* TODO: better way ??? *)
|
||||
let globals_min_id : data = 1000
|
||||
|
||||
let prog_init (prog : prog) : state =
|
||||
match prog with (decls, _) -> fst @@ List.fold_left (* TODO: FIXME: check x's order *)
|
||||
(fun (st, x) d -> (add_decl st x d, x + 1))
|
||||
(empty_state, globals_min_id)
|
||||
decls
|
||||
|
||||
(* - call values spoil *)
|
||||
|
||||
(* TODO: check assignment type matches types separately later ?? *)
|
||||
let is_correct_tags (r : read_cap) (w : write_cap)
|
||||
(m : mode) (c : copy_cap) : bool =
|
||||
(mode_out m != Out || c == Rf) &&
|
||||
(mode_out m != Out || w == AlwaysWr || w == UndefWr) &&
|
||||
(r != Rd || mode_in m == In)
|
||||
(snd m != Out || c == Rf) &&
|
||||
(snd m != Out || w == AlwaysWr) &&
|
||||
(r != Rd || fst m == In)
|
||||
|
||||
let tryread (r : read_cap) (v_m : memval)
|
||||
(v_r : readval) (v_w : writeval) : value =
|
||||
|
|
@ -368,16 +359,14 @@ struct
|
|||
| Rd -> UnitV (memvmod ReadA v_m,
|
||||
readvmod ReadA v_r,
|
||||
writevmod ReadA v_w)
|
||||
| NRd -> UnitV (v_m, v_r, v_w)
|
||||
| UndefRd -> raise @@ Cant_deduce_rw_error "tryread"
|
||||
| NRd -> UnitV (v_m, v_r, v_w)
|
||||
|
||||
let tryspoil (m : mode) (w : write_cap) (v_m : memval) : memval =
|
||||
match m, w with
|
||||
| Mode (_, Out), AlwaysWr -> v_m
|
||||
| Mode (_, Out), MayWr -> v_m
|
||||
| Mode (_, NOut), AlwaysWr -> BotMV
|
||||
| Mode (_, NOut), MayWr -> SmthMV
|
||||
| _, UndefWr -> raise @@ Cant_deduce_rw_error "tryspoil"
|
||||
| (_, Out), AlwaysWr -> v_m
|
||||
| (_, Out), MayWr -> v_m
|
||||
| (_, NOut), AlwaysWr -> BotMV
|
||||
| (_, NOut), MayWr -> SmthMV
|
||||
| _ -> raise @@ Typing_error "tryspoil: unexpected pair mode + write cap"
|
||||
|
||||
let rec valspoil (mem : mem) (v : value) (t : atype)
|
||||
|
|
@ -397,12 +386,10 @@ struct
|
|||
then (memvmod AlwaysWriteA v_m',
|
||||
readvmod AlwaysWriteA v_r',
|
||||
writevmod AlwaysWriteA v_w')
|
||||
else if w == UndefWr
|
||||
then raise @@ Cant_deduce_rw_error "valspoil"
|
||||
else (* MayWr *)
|
||||
(memvmod MayWriteA v_m',
|
||||
readvmod MayWriteA v_r',
|
||||
writevmod MayWriteA v_w'))
|
||||
else (* MayWr *)
|
||||
(memvmod MayWriteA v_m',
|
||||
readvmod MayWriteA v_r',
|
||||
writevmod MayWriteA v_w'))
|
||||
in
|
||||
let v_m''' = tryspoil m w v_m'' in
|
||||
(mem, UnitV (v_m''', v_r'', v_w''))
|
||||
|
|
@ -453,42 +440,32 @@ struct
|
|||
|
||||
(* --- *)
|
||||
|
||||
let readval_to_cap (v_w : readval) : read_cap =
|
||||
match v_w with
|
||||
| ZeroRV -> NRd
|
||||
| OneRV -> Rd
|
||||
| TopRV -> NRd
|
||||
|
||||
let writeval_to_cap (v_w : writeval) : write_cap =
|
||||
match v_w with
|
||||
| ZeroWV -> NeverWr
|
||||
| SmthWV -> MayWr
|
||||
| OneWV -> AlwaysWr
|
||||
|
||||
(* NOTE: in analyzer rw tags check replaces tags with calculated ones *)
|
||||
let rec tags_check (mem : mem) (v : value) (t : atype) : atype =
|
||||
let rec tags_check (mem : mem) (v : value) (t : atype) : unit =
|
||||
match v, t with
|
||||
| UnitV (v_m, v_r, v_w), UnitT (r, w) ->
|
||||
let r' = readval_to_cap v_r in
|
||||
let w' = writeval_to_cap v_w in
|
||||
if r != UndefRd && r != r'
|
||||
then raise @@ Eval_error "tags_check: not undef read tag & not correct"
|
||||
else if w != UndefWr && w != w'
|
||||
then raise @@ Eval_error "tags_check: not undef write tag & not correct"
|
||||
else UnitT (r', w')
|
||||
| FunV, FunT _ -> t
|
||||
| RefV id, RefT (c, t) -> RefT (c, tags_check mem (mem_get mem id) t)
|
||||
| TupleV vs, TupleT ts -> TupleT (List.map2 (tags_check mem) vs ts)
|
||||
if (r == Rd) && (v_r != OneRV)
|
||||
then raise @@ Eval_error "tags_check: wrong read tag"
|
||||
else if (r == NRd) && (v_r == OneRV)
|
||||
then raise @@ Eval_error "tags_check: wrong not read tag"
|
||||
else if writeval_to_cap v_w != w
|
||||
then raise @@ Eval_error "tags_check: wrong write tag"
|
||||
else ()
|
||||
| FunV, FunT _ -> ()
|
||||
| RefV id, RefT (_, t) -> tags_check mem (mem_get mem id) t
|
||||
| TupleV vs, TupleT ts -> ignore @@ List.map2 (tags_check mem) vs ts
|
||||
| _, _ -> raise @@ Typing_error "tags_check"
|
||||
|
||||
(* - writability check *)
|
||||
|
||||
let rec is_all_type_writable (t : atype) : bool =
|
||||
match t with
|
||||
| UnitT (_, MayWr) -> true
|
||||
| UnitT (_, AlwaysWr) -> true
|
||||
| UnitT (_, NeverWr) -> false
|
||||
| UnitT (_, UndefWr) -> true (* NOTE: tag is not deduced yet, consider writable *)
|
||||
| UnitT (_, w) -> w == MayWr || w == AlwaysWr
|
||||
| FunT _ -> true
|
||||
| RefT (_, t) -> is_all_type_writable t
|
||||
| TupleT ts -> List.for_all is_all_type_writable ts
|
||||
|
|
@ -537,51 +514,28 @@ struct
|
|||
|
||||
(* - function evaluation *)
|
||||
|
||||
let rec replace_rw_undef_with_r_aw (t : atype) : atype = match t with
|
||||
| UnitT (r, w) -> let r' = if r == UndefRd then Rd else r in
|
||||
let w' = if w == UndefWr then AlwaysWr else w in
|
||||
UnitT (r', w')
|
||||
| RefT (c, t) -> RefT (c, replace_rw_undef_with_r_aw t)
|
||||
| TupleT ts -> TupleT (List.map replace_rw_undef_with_r_aw ts)
|
||||
| FunT ts -> FunT ts (* NOTE: can't properly deduce *)
|
||||
|
||||
(* NOTE: in analyzer rw replaces read & write tags with calculated ones *)
|
||||
let rec func_eval (state : state) (d : decl) : decl =
|
||||
let rec func_eval (state : state) (d : decl) : unit =
|
||||
match d with
|
||||
| FunD (ts, stmt) ->
|
||||
(let (state_with_args, _) = List.fold_left
|
||||
(fun (st, x) (m, t) -> (addarg st x t, x + 1))
|
||||
(state, 0) ts in
|
||||
match stmt_eval state_with_args stmt with (mem_after_stmt, _, vals_after_stmt) ->
|
||||
let (_, ts') = List.fold_left
|
||||
(fun (x, ts_acc) (m, t) ->
|
||||
ignore @@ List.fold_left
|
||||
(fun x (_, t) ->
|
||||
let id = vals_assoc x vals_after_stmt in
|
||||
let v = mem_get mem_after_stmt id in
|
||||
let t' = tags_check mem_after_stmt v t in
|
||||
(x + 1, (m, t') :: ts_acc))
|
||||
(0, []) ts in
|
||||
(* TODO: FIXME: isure that need reverse ? *)
|
||||
FunD (List.rev ts', stmt))
|
||||
(* NOTE: tags for globals not checked and not important in current implementation *)
|
||||
| VarD t -> VarD (replace_rw_undef_with_r_aw t)
|
||||
tags_check mem_after_stmt v t; x + 1)
|
||||
0 ts)
|
||||
| VarD _ -> ()
|
||||
|
||||
(* --- program execution --- *)
|
||||
|
||||
(* NOTE: decls returned in the reversed order (?) *)
|
||||
let prog_init (prog : prog) : (state * decl list) =
|
||||
match prog with (decls, _) -> let (st', decls', _) = List.fold_left (* TODO: FIXME: check x's order *)
|
||||
(fun (st, decls', x) d ->
|
||||
let d' = func_eval st d in
|
||||
(add_decl st x d', d' :: decls', x + 1))
|
||||
(empty_state, [], globals_min_id)
|
||||
decls in
|
||||
(st', List.rev decls')
|
||||
|
||||
let prog_eval (prog : prog) : prog =
|
||||
let prog_eval (prog : prog) : state =
|
||||
match prog with (decls, s) ->
|
||||
let (init_state, decls') = prog_init prog in
|
||||
ignore @@ stmt_eval init_state s;
|
||||
(decls', s)
|
||||
let init_state = prog_init prog in
|
||||
ignore @@ List.map (func_eval init_state) decls;
|
||||
stmt_eval init_state s
|
||||
|
||||
let prog_eval_noret (prog : prog) : unit =
|
||||
ignore @@ prog_eval prog
|
||||
|
|
@ -649,12 +603,11 @@ struct
|
|||
let uT_mw = UnitT (NRd, MayWr)
|
||||
let uT_r = UnitT (Rd, NeverWr)
|
||||
let uT = UnitT (NRd, NeverWr)
|
||||
let uT_undef = UnitT (UndefRd, UndefWr)
|
||||
|
||||
let rfT t = RefT (Rf, t)
|
||||
let cpT t = RefT (Cp, t)
|
||||
|
||||
let moded t = (Mode (In, NOut), t)
|
||||
let moded t = ((In, NOut), t)
|
||||
|
||||
let defg t = VarD t
|
||||
|
||||
|
|
@ -688,86 +641,6 @@ struct
|
|||
(v_memval_is (mem_get mem id3) SmthMV);
|
||||
[%expect {| 0 1 2 true true true true true true |}]
|
||||
|
||||
(* - simple rw tags gen tests *)
|
||||
|
||||
let%expect_test "simple call with read, dsl, rw gen" =
|
||||
let prog' = prog_eval (
|
||||
[
|
||||
defg (rfT uT_r_mw);
|
||||
FunD (
|
||||
[moded @@ cpT @@ uT_undef],
|
||||
rdS @@ drf @@ v0
|
||||
)
|
||||
],
|
||||
callS vg1 [pE vg0]
|
||||
) in
|
||||
prog_eval_noret prog';
|
||||
print_endline @@ show(prog) prog';
|
||||
[%expect {| ([VarD (RefT (Rf, UnitT (Rd, MayWr))); FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))], ReadS (DerefP (VarP (0))))], CallS (VarP (1001), [PathE (VarP (1000))])) |}]
|
||||
|
||||
let%expect_test "presentation test 1 (simple types), dsl, rw gen" =
|
||||
let prog' = prog_eval (
|
||||
[
|
||||
defg (rfT uT_r_aw); (* x *)
|
||||
defg (rfT uT_r_aw); (* y *)
|
||||
defg (rfT uT_r_aw); (* z *)
|
||||
defg (rfT uT_r_aw); (* k *)
|
||||
FunD ( (* f *)
|
||||
[
|
||||
(moded @@ rfT @@ uT_undef);
|
||||
(moded @@ rfT @@ uT_undef);
|
||||
],
|
||||
(rdS @@ drf @@ v0) #.
|
||||
(wrS @@ drf @@ v0) #.
|
||||
(rdS @@ drf @@ v1)
|
||||
);
|
||||
FunD ( (* w *)
|
||||
[
|
||||
(moded @@ cpT @@ uT_undef);
|
||||
],
|
||||
(wrS @@ drf @@ v0) |. skp
|
||||
);
|
||||
FunD ( (* g *)
|
||||
[
|
||||
(moded @@ rfT @@ uT_undef);
|
||||
(moded @@ cpT @@ uT_undef);
|
||||
],
|
||||
(wrS @@ drf @@ v0) #.
|
||||
((wrS @@ drf @@ v1) |. (wrS @@ drf @@ v0)) #.
|
||||
(rdS @@ drf @@ v0) #.
|
||||
(rdS @@ drf @@ v1)
|
||||
);
|
||||
FunD ( (* r *)
|
||||
[
|
||||
(moded @@ rfT @@ uT_undef);
|
||||
],
|
||||
(rdS @@ drf @@ v0)
|
||||
)
|
||||
],
|
||||
let xV = vg0 in
|
||||
let yV = vg1 in
|
||||
let zV = vg2 in
|
||||
let kV = vg3 in
|
||||
let fF = vg4 in
|
||||
let wF = vg5 in
|
||||
let gF = vg6 in
|
||||
let rF = vg7 in
|
||||
(callS wF [pE xV]) #.
|
||||
(callS rF [pE xV]) #.
|
||||
(callS fF [pE xV; pE yV]) #.
|
||||
(callS rF [pE yV]) #.
|
||||
(callS gF [pE zV; pE kV]) #.
|
||||
(wrS @@ drf @@ zV) #.
|
||||
(callS wF [pE zV]) #.
|
||||
(callS fF [pE yV; pE zV]) #.
|
||||
(callS rF [pE kV])
|
||||
) in
|
||||
prog_eval_noret prog';
|
||||
print_endline @@ show(prog) prog';
|
||||
[%expect {| ([VarD (RefT (Rf, UnitT (Rd, AlwaysWr))); VarD (RefT (Rf, UnitT (Rd, AlwaysWr))); VarD (RefT (Rf, UnitT (Rd, AlwaysWr))); VarD (RefT (Rf, UnitT (Rd, AlwaysWr))); FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))], SeqS (SeqS (ReadS (DerefP (VarP (0))), WriteS (DerefP (VarP (0)))), ReadS (DerefP (VarP (1))))); FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, MayWr)))], ChoiceS (WriteS (DerefP (VarP (0))), SkipS)); FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))], SeqS (SeqS (SeqS (WriteS (DerefP (VarP (0))), ChoiceS (WriteS (DerefP (VarP (1))), WriteS (DerefP (VarP (0))))), ReadS (DerefP (VarP (0)))), ReadS (DerefP (VarP (1))))); FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))], ReadS (DerefP (VarP (0))))], SeqS (SeqS (SeqS (SeqS (SeqS (SeqS (SeqS (SeqS (CallS (VarP (1005), [PathE (VarP (1000))]), CallS (VarP (1007), [PathE (VarP (1000))])), CallS (VarP (1004), [PathE (VarP (1000)); PathE (VarP (1001))])), CallS (VarP (1007), [PathE (VarP (1001))])), CallS (VarP (1006), [PathE (VarP (1002)); PathE (VarP (1003))])), WriteS (DerefP (VarP (1002)))), CallS (VarP (1005), [PathE (VarP (1002))])), CallS (VarP (1004), [PathE (VarP (1001)); PathE (VarP (1002))])), CallS (VarP (1007), [PathE (VarP (1003))]))) |}]
|
||||
|
||||
(* TODO *)
|
||||
|
||||
(* - basic var tests *)
|
||||
|
||||
let%expect_test "empty" =
|
||||
|
|
@ -967,23 +840,23 @@ struct
|
|||
Printf.printf "done!";
|
||||
[%expect {| done! |}]
|
||||
|
||||
(* NOTE: does not work for annalyzer rw to the sequenced declaration addition to calculate tags *)
|
||||
(* let%expect_test "call inside call, recursive, dsl" = *)
|
||||
(* prog_eval_noret ( *)
|
||||
(* [ *)
|
||||
(* defg uT_r_aw; *)
|
||||
(* defg (rfT uT_r_aw); *)
|
||||
(* FunD ( *)
|
||||
(* [moded @@ cpT @@ uT_aw], *)
|
||||
(* (callS vg2 [pE v0]) #. *)
|
||||
(* (wrS @@ drf @@ v0) *)
|
||||
(* ) *)
|
||||
(* ], *)
|
||||
(* (callS vg2 [pE vg1]) #. *)
|
||||
(* (rdS @@ drf @@ vg1) *)
|
||||
(* ); *)
|
||||
(* Printf.printf "done!"; *)
|
||||
(* [%expect {| done! |}] *)
|
||||
(* NOTE: memoization used *)
|
||||
let%expect_test "call inside call, recursive, dsl" =
|
||||
prog_eval_noret (
|
||||
[
|
||||
defg uT_r_aw;
|
||||
defg (rfT uT_r_aw);
|
||||
FunD (
|
||||
[moded @@ cpT @@ uT_aw],
|
||||
(callS vg2 [pE v0]) #.
|
||||
(wrS @@ drf @@ v0)
|
||||
)
|
||||
],
|
||||
(callS vg2 [pE vg1]) #.
|
||||
(rdS @@ drf @@ vg1)
|
||||
);
|
||||
Printf.printf "done!";
|
||||
[%expect {| done! |}]
|
||||
|
||||
let%expect_test "call to fix after call, dsl" =
|
||||
prog_eval_noret (
|
||||
|
|
@ -995,7 +868,7 @@ struct
|
|||
wrS @@ drf @@ v0
|
||||
);
|
||||
FunD (
|
||||
[(Mode (In, Out), rfT @@ uT_aw)],
|
||||
[((In, Out), rfT @@ uT_aw)],
|
||||
wrS @@ drf @@ v0
|
||||
)
|
||||
],
|
||||
|
|
@ -1057,10 +930,10 @@ struct
|
|||
defg (rfT uT_r_aw);
|
||||
FunD (
|
||||
[
|
||||
(Mode (NIn, NOut), cpT @@ uT);
|
||||
(Mode (In, NOut), cpT @@ uT_r_aw);
|
||||
(Mode (NIn, Out), rfT @@ uT_aw);
|
||||
(Mode (In, Out), rfT @@ uT_r_aw);
|
||||
((NIn, NOut), cpT @@ uT);
|
||||
((In, NOut), cpT @@ uT_r_aw);
|
||||
((NIn, Out), rfT @@ uT_aw);
|
||||
((In, Out), rfT @@ uT_r_aw);
|
||||
],
|
||||
(rdS @@ drf @@ v1) #.
|
||||
(rdS @@ drf @@ v3) #.
|
||||
|
|
@ -1091,10 +964,10 @@ struct
|
|||
defg (rfT uT_r_aw);
|
||||
FunD (
|
||||
[
|
||||
(Mode (NIn, NOut), rfT @@ uT);
|
||||
(Mode (In, NOut), rfT @@ uT_r);
|
||||
(Mode (NIn, Out), rfT @@ uT_aw);
|
||||
(Mode (In, Out), rfT @@ uT_r_aw);
|
||||
((NIn, NOut), rfT @@ uT);
|
||||
((In, NOut), rfT @@ uT_r);
|
||||
((NIn, Out), rfT @@ uT_aw);
|
||||
((In, Out), rfT @@ uT_r_aw);
|
||||
],
|
||||
(rdS @@ drf @@ v1) #.
|
||||
(rdS @@ drf @@ v3) #.
|
||||
|
|
@ -1177,98 +1050,129 @@ struct
|
|||
Printf.printf "done!";
|
||||
[%expect {| done! |}]
|
||||
|
||||
let%expect_test "presentation test 2 (complex types), dsl, rw gen" =
|
||||
let prog' = prog_eval (
|
||||
let userT = TupleT [uT_undef; uT_undef; uT_undef] in
|
||||
let dataT = TupleT [uT_undef; uT_undef] in
|
||||
let requestT = TupleT [cpT userT;
|
||||
cpT dataT;
|
||||
cpT uT_undef] in
|
||||
let requestArgsT = TupleT [cpT userT;
|
||||
rfT dataT;
|
||||
rfT uT_undef] in
|
||||
[
|
||||
defg requestT;
|
||||
FunD ( (* send *)
|
||||
[
|
||||
(moded @@ requestArgsT)
|
||||
],
|
||||
((
|
||||
(rdS @@ drf @@ access 1 @@ v0) #.
|
||||
(wrS @@ drf @@ access 1 @@ v0) #.
|
||||
(rdS v0) #.
|
||||
(wrS @@ access 1 @@ drf @@ access 0 @@ v0)
|
||||
) |.
|
||||
skp) #.
|
||||
(wrS @@ drf @@ access 2 @@ v0) #.
|
||||
(rdS v0)
|
||||
);
|
||||
],
|
||||
(callS vg1 [pE vg0]) #.
|
||||
(wrS @@ drf @@ access 2 @@ vg0) #.
|
||||
((rdS @@ access 1 @@ drf @@ access 0 @@ vg0) |.
|
||||
(rdS @@ access 2 @@ drf @@ access 0 @@ vg0)) #.
|
||||
(rdS @@ drf @@ access 2 @@ vg0)
|
||||
) in
|
||||
prog_eval_noret prog';
|
||||
print_endline @@ show(prog) prog';
|
||||
[%expect {| ([VarD (TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr))])); FunD ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, MayWr); UnitT (Rd, NeverWr)])); RefT (Rf, TupleT ([UnitT (Rd, MayWr); UnitT (Rd, MayWr)])); RefT (Rf, UnitT (Rd, AlwaysWr))]))], SeqS (SeqS (ChoiceS (SeqS (SeqS (SeqS (ReadS (DerefP (AccessP (VarP (0), 1))), WriteS (DerefP (AccessP (VarP (0), 1)))), ReadS (VarP (0))), WriteS (AccessP (DerefP (AccessP (VarP (0), 0)), 1))), SkipS), WriteS (DerefP (AccessP (VarP (0), 2)))), ReadS (VarP (0))))], SeqS (SeqS (SeqS (CallS (VarP (1001), [PathE (VarP (1000))]), WriteS (DerefP (AccessP (VarP (1000), 2)))), ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (1000), 0)), 1)), ReadS (AccessP (DerefP (AccessP (VarP (1000), 0)), 2)))), ReadS (DerefP (AccessP (VarP (1000), 2))))) |}]
|
||||
(* TODO tags, access *)
|
||||
(* let%expect_test "presentation test 2 (complex types), dsl" = *)
|
||||
(* prog_eval_noret ( *)
|
||||
(* let userT = TupleT [uT_r_aw; uT_r_aw; uT_r_aw] in *)
|
||||
(* let dataT = TupleT [uT_r_aw; uT_r_aw] in *)
|
||||
(* let requestT = TupleT [cpT userT; *)
|
||||
(* cpT dataT; *)
|
||||
(* cpT dataT] in *)
|
||||
(* let requestArgsT = TupleT [cpT userT; (* TODO: tags *) *)
|
||||
(* cpT dataT; *)
|
||||
(* cpT dataT] in *)
|
||||
(* let userE = TupleE [UnitE; UnitE; UnitE] in *)
|
||||
(* let dataE = TupleE [UnitE; UnitE] in *)
|
||||
(* let requestE = TupleE [rfg0E; rfg1E; rfg2E] in *)
|
||||
(* [ *)
|
||||
(* defg userT userE; *)
|
||||
(* defg dataT dataE; *)
|
||||
(* defg uT_r_aw; (* time *) *)
|
||||
(* defg requestT requestE; *)
|
||||
(* FunD ( (* send *) *)
|
||||
(* [ *)
|
||||
(* (moded @@ requestArgsT) *)
|
||||
(* ], *)
|
||||
(* ( *)
|
||||
(* ( (* TODO access *) *)
|
||||
(* (rdS @@ drf @@ v0) #. *)
|
||||
(* (wrS @@ drf @@ v0) #. *)
|
||||
(* (rdS @@ drf @@ v0) #. *)
|
||||
(* (wrS @@ drf @@ v0) *)
|
||||
(* ) |. *)
|
||||
(* skp) #. *)
|
||||
(* TODO access *)
|
||||
(* (wrS @@ drf @@ v0) #. *)
|
||||
(* (rdS @@ drf @@ v1) *)
|
||||
(* ); *)
|
||||
(* ], *)
|
||||
(* (callS vg4 [pE vg3]) #. *)
|
||||
(* TODO access *)
|
||||
(* (wrS @@ drf @@ vg3) #. *)
|
||||
(* ((rdS @@ drf @@ vg3) |. (rdS @@ drf @@ vg3)) #. *)
|
||||
(* (rdS @@ drf @@ vg3) *)
|
||||
(* ); *)
|
||||
(* Printf.printf "done!"; *)
|
||||
(* [%expect {| done! |}] *)
|
||||
|
||||
(* - complex tests *)
|
||||
|
||||
let%expect_test "complex test: send, dsl" =
|
||||
let prog' = prog_eval (
|
||||
(* TODO: FIXME: rw tags *)
|
||||
(* NOTE: path access isreversed to intuitive function application
|
||||
by definition *)
|
||||
(* let%expect_test "complex test: send, dsl" = *)
|
||||
(* prog_eval_noret ( *)
|
||||
(* TODO: set optimal ref mods later *)
|
||||
let user_utilsT = TupleT [uT_undef (* 0 id *); uT_undef] in
|
||||
let user_infoT = TupleT [uT_undef (* 0 name *); uT_undef; uT_undef] in
|
||||
let userT = TupleT [cpT user_utilsT (* 0 utils *); cpT user_infoT (* 1 info *)] in
|
||||
let versionT = TupleT [uT_undef (* 0 id *); uT_undef; uT_undef] in
|
||||
let utilsT = TupleT [uT_undef (* 0 has_version *); uT_undef (* 1 id *)] in
|
||||
let requestT = TupleT [cpT userT (* 0 user *);
|
||||
cpT versionT (* 1 version *);
|
||||
cpT utilsT (* 2 utils *);
|
||||
cpT uT_undef (* 3 data *);
|
||||
uT_undef (* 4 operation_date *)] in
|
||||
let get_version_idID = vg1 in
|
||||
let updated_versionID = vg2 in
|
||||
let sendID = vg3 in
|
||||
let send_allID = vg4 in
|
||||
let get_version_idF = FunD ([moded requestT],
|
||||
(rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in
|
||||
let updated_versionF = FunD ([moded requestT],
|
||||
(rdS @@ access 0 @@ drf @@ access 2 v0) #.
|
||||
(* let user_utilsT = TupleT [uT_r_aw (* 0 id *); uT_r_aw] in *)
|
||||
(* let user_infoT = TupleT [uT_r_aw (* 0 name *); uT_r_aw; uT_r_aw] in *)
|
||||
(* let userT = TupleT [cpT user_utilsT (* 0 utils *); cpT user_infoT (* 1 info *)] in *)
|
||||
(* let versionT = TupleT [uT_r_aw (* 0 id *); uT_r_aw; uT_r_aw] in *)
|
||||
(* let utilsT = TupleT [uT_r_aw (* 0 has_version *); uT_r_aw (* 1 id *)] in *)
|
||||
(* let requestT = TupleT [cpT userT (* 0 user *); *)
|
||||
(* cpT versionT (* 1 version *); *)
|
||||
(* cpT utilsT (* 2 utils *); *)
|
||||
(* cpT uT_r_aw (* 3 data *); *)
|
||||
(* uT_r_aw (* 4 operation_date *)] in *)
|
||||
(* let user_utilsE = TupleE [UnitE (* 0 id *); UnitE] in *)
|
||||
(* let user_infoE = TupleE [UnitE (* 0 name *); UnitE; UnitE] in *)
|
||||
(* let userE = TupleE [rfg0E (* 0 utils *); rfg1E (* 1 info *)] in *)
|
||||
(* let versionE = TupleE [UnitE (* 0 id *); UnitE; UnitE] in *)
|
||||
(* let utilsE = TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] in *)
|
||||
(* let requestE = TupleE [rfg2E (* 0 user *); *)
|
||||
(* rfg3E (* 1 version *); *)
|
||||
(* rfg4E (* 2 utils *); *)
|
||||
(* rfg5E (* 3 data *); *)
|
||||
(* UnitE (* 4 operation_date *)] in *)
|
||||
(* let get_version_idID = vg7 in *)
|
||||
(* let updated_versionID = vg8 in *)
|
||||
(* let sendID = vg9 in *)
|
||||
(* let send_allID = vg10 in *)
|
||||
(* let get_version_idF = FunD ([moded requestT], *)
|
||||
(* (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in *)
|
||||
(* 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
|
||||
let sendF = FunD ([moded requestT],
|
||||
((
|
||||
(wrS @@ access 0 @@ drf @@ access 2 v0) #.
|
||||
(rdS @@ drf @@ access 3 v0) #.
|
||||
(wrS @@ drf @@ access 3 v0) #.
|
||||
(rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0)
|
||||
) |. skp) #.
|
||||
(wrS @@ access 4 v0) #.
|
||||
(rdS v0)) in
|
||||
let send_allF = FunD ([moded requestT],
|
||||
(wrS v0) #.
|
||||
(callS sendID [pE v0]) #.
|
||||
(callS get_version_idID [pE v0]) #.
|
||||
(callS updated_versionID [pE v0]) #.
|
||||
(wrS @@ drf @@ access 1 v0) #. (* TODO: check, all required substruct ? *)
|
||||
(* (rdS @@ access 0 @@ drf @@ access 1 v0) #. *)
|
||||
(* (rdS @@ access 1 @@ drf @@ access 1 v0)) in *)
|
||||
(* let sendF = FunD ([moded requestT], *)
|
||||
(* (( *)
|
||||
(* (wrS @@ access 0 @@ drf @@ access 2 v0) #. *)
|
||||
(* (rdS @@ 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 *) *)
|
||||
(* let send_allF = FunD ([moded requestT], *)
|
||||
(* (wrS @@ access 4 v0) (*wrS v0*) #. (* FIXME: TMP, parial write, should be full *) *)
|
||||
(* (callS sendID [pE v0]) #. *)
|
||||
(* (callS get_version_idID [pE v0]) #. *)
|
||||
(* (callS updated_versionID [pE v0]) #. *)
|
||||
(* TODO: read all the substructure ?? *)
|
||||
(* (wrS @@ access 0 @@ 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 1 v0))) in
|
||||
let varID = vg0 in
|
||||
[
|
||||
defg requestT;
|
||||
get_version_idF;
|
||||
updated_versionF;
|
||||
sendF;
|
||||
send_allF
|
||||
],
|
||||
callS send_allID [pE varID]
|
||||
) in
|
||||
prog_eval_noret prog';
|
||||
print_endline @@ show(prog) prog';
|
||||
[%expect {| ([VarD (TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr)); UnitT (Rd, AlwaysWr)])); FunD ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)])); RefT (Cp, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)])); RefT (Cp, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)])); RefT (Cp, UnitT (NRd, NeverWr)); UnitT (NRd, NeverWr)]))], ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (0), 1)), 0)), SkipS)); FunD ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)])); RefT (Cp, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, NeverWr); UnitT (NRd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (NRd, NeverWr)])); RefT (Cp, UnitT (NRd, NeverWr)); UnitT (NRd, NeverWr)]))], SeqS (SeqS (ReadS (AccessP (DerefP (AccessP (VarP (0), 2)), 0)), ReadS (AccessP (DerefP (AccessP (VarP (0), 1)), 0))), ReadS (AccessP (DerefP (AccessP (VarP (0), 1)), 1)))); FunD ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, NeverWr); UnitT (Rd, NeverWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, NeverWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, MayWr); UnitT (Rd, NeverWr)])); RefT (Cp, UnitT (Rd, MayWr)); UnitT (NRd, AlwaysWr)]))], SeqS (SeqS (ChoiceS (SeqS (SeqS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (0), 2)), 0)), ReadS (DerefP (AccessP (VarP (0), 3)))), WriteS (DerefP (AccessP (VarP (0), 3)))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (0), 0)), 1)), 0))), SkipS), WriteS (AccessP (VarP (0), 4))), ReadS (VarP (0)))); FunD ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr)]))])); RefT (Cp, TupleT ([UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr)])); RefT (Cp, UnitT (NRd, AlwaysWr)); UnitT (NRd, AlwaysWr)]))], SeqS (SeqS (SeqS (SeqS (SeqS (WriteS (VarP (0)), CallS (VarP (1003), [PathE (VarP (0))])), CallS (VarP (1001), [PathE (VarP (0))])), CallS (VarP (1002), [PathE (VarP (0))])), WriteS (DerefP (AccessP (VarP (0), 1)))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (0), 0)), 0)), 0)), ReadS (AccessP (DerefP (AccessP (VarP (0), 1)), 0)))))], CallS (VarP (1004), [PathE (VarP (1000))])) |}]
|
||||
(* ((rdS @@ access 0 @@ drf @@ access 0 @@ drf @@ access 0 v0) |. *)
|
||||
(* (rdS @@ access 0 @@ drf @@ access 1 v0))) in *)
|
||||
(* let varID = vg6 in *)
|
||||
(* [ *)
|
||||
(* defg user_utilsT user_utilsE; *)
|
||||
(* defg user_infoT user_infoE; *)
|
||||
(* defg userT userE; *)
|
||||
(* defg versionT versionE; *)
|
||||
(* defg utilsT utilsE; *)
|
||||
(* defg uT_r_aw; *)
|
||||
(* defg requestT requestE; *)
|
||||
(* get_version_idF; *)
|
||||
(* updated_versionF; *)
|
||||
(* sendF; *)
|
||||
(* send_allF *)
|
||||
(* ], *)
|
||||
(* callS send_allID [pE varID] *)
|
||||
(* ); *)
|
||||
(* Printf.printf "done!"; *)
|
||||
(* [%expect {| done! |}] *)
|
||||
|
||||
(* TODO: version with more optimal modifiers *)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -107,6 +107,3 @@ let%expect_test "presentation test 2 (complex types), synt" = print_endline(prog
|
|||
(* let%expect_test "complex test: send" = print_endline(prog_synt_compl_test_send ()); *)
|
||||
(* [%expect {| [[Rf; Cp; Cp; Cp; Cp; Cp]; [Cp; Cp; Cp; Cp; Cp; Cp]] |}] (* TODO: FIXME *) *)
|
||||
(* TODO *)
|
||||
|
||||
let%expect_test "complex test: send, gen rw" = print_endline(prog_synt_compl_test_send_gen_rw ());
|
||||
[%expect {| [[Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Cp; Rf; Rf; Rf; Rf; Rf; Rf; Rf]] |}]
|
||||
|
|
|
|||
|
|
@ -1357,62 +1357,3 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
|
|||
) &
|
||||
prog_evalo prog st })
|
||||
(fun q -> q#reify (List.prj_exn CopyCap.prj_exn))))
|
||||
|
||||
(* complex test with already generated rw tags *)
|
||||
|
||||
let prog_synt_compl_test_send_gen_rw _ = show(answerCpCapList) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, st,
|
||||
c00, c01, c02, c03, c04, c05,
|
||||
c10, c11, c12, c13, c14, c15,
|
||||
c20, c21, c22, c23, c24, c25,
|
||||
c30, c31, c32, c33, c34, c35
|
||||
in
|
||||
|
||||
q == [
|
||||
c00; c01; c02; c03; c04; c05;
|
||||
c10; c11; c12; c13; c14; c15;
|
||||
c20; c21; c22; c23; c24; c25;
|
||||
c30; c31; c32; c33; c34; c35
|
||||
] &
|
||||
|
||||
c00 == Rf &
|
||||
c01 == Rf &
|
||||
c02 == Rf &
|
||||
c03 == Rf &
|
||||
c04 == Rf &
|
||||
c05 == Rf &
|
||||
c10 == Rf &
|
||||
c11 == Rf &
|
||||
c12 == Rf &
|
||||
c13 == Rf &
|
||||
c14 == Rf &
|
||||
c15 == Rf &
|
||||
c20 == Rf &
|
||||
c21 == Rf &
|
||||
c22 == Rf &
|
||||
c23 == Rf &
|
||||
c24 == Cp &
|
||||
c25 == Rf &
|
||||
c30 == Rf &
|
||||
c31 == Rf &
|
||||
c32 == Rf &
|
||||
c33 == Rf &
|
||||
c34 == Rf &
|
||||
c35 == Rf &
|
||||
|
||||
prog == Prg ([
|
||||
VarD (TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr)); UnitT (Rd, AlwaysWr)]));
|
||||
FunD ([(Mode (In, NOut), TupleT ([RefT (c00, TupleT ([RefT (c01, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)])); RefT (c02, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)]))])); RefT (c03, TupleT ([UnitT (Rd, NeverWr); UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)])); RefT (c04, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)])); RefT (c05, UnitT (NRd, NeverWr)); UnitT (NRd, NeverWr)]))],
|
||||
ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (0), 1)), 0)), SkipS));
|
||||
FunD ([(Mode (In, NOut), TupleT ([RefT (c10, TupleT ([RefT (c11, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)])); RefT (c12, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)]))])); RefT (c13, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, NeverWr); UnitT (NRd, NeverWr)])); RefT (c14, TupleT ([UnitT (Rd, NeverWr); UnitT (NRd, NeverWr)])); RefT (c15, UnitT (NRd, NeverWr)); UnitT (NRd, NeverWr)]))],
|
||||
SeqS (SeqS (ReadS (AccessP (DerefP (AccessP (VarP (0), 2)), 0)), ReadS (AccessP (DerefP (AccessP (VarP (0), 1)), 0))), ReadS (AccessP (DerefP (AccessP (VarP (0), 1)), 1))));
|
||||
FunD ([(Mode (In, NOut), TupleT ([RefT (c20, TupleT ([RefT (c21, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, NeverWr)])); RefT (c22, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, NeverWr); UnitT (Rd, NeverWr)]))])); RefT (c23, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, NeverWr); UnitT (Rd, NeverWr)])); RefT (c24, TupleT ([UnitT (Rd, MayWr); UnitT (Rd, NeverWr)])); RefT (c25, UnitT (Rd, MayWr)); UnitT (NRd, AlwaysWr)]))],
|
||||
SeqS (SeqS (ChoiceS (SeqS (SeqS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (0), 2)), 0)), ReadS (DerefP (AccessP (VarP (0), 3)))), WriteS (DerefP (AccessP (VarP (0), 3)))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (0), 0)), 1)), 0))), SkipS), WriteS (AccessP (VarP (0), 4))), ReadS (VarP (0))));
|
||||
FunD ([(Mode (In, NOut), TupleT ([RefT (c30, TupleT ([RefT (c31, TupleT ([UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr)])); RefT (c32, TupleT ([UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr)]))])); RefT (c33, TupleT ([UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr)])); RefT (c34, TupleT ([UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr)])); RefT (c35, UnitT (NRd, AlwaysWr)); UnitT (NRd, AlwaysWr)]))],
|
||||
SeqS (SeqS (SeqS (SeqS (SeqS (WriteS (VarP (0)), CallS (VarP (13), [PathE (VarP (0))])), CallS (VarP (11), [PathE (VarP (0))])), CallS (VarP (12), [PathE (VarP (0))])), WriteS (DerefP (AccessP (VarP (0), 1)))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (0), 0)), 0)), 0)), ReadS (AccessP (DerefP (AccessP (VarP (0), 1)), 0)))))
|
||||
],
|
||||
CallS (VarP (14), [PathE (VarP (10))])
|
||||
) &
|
||||
prog_evalo prog st })
|
||||
(fun q -> q#reify (List.prj_exn CopyCap.prj_exn))))
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue