mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-06-11 03:38:15 +00:00
Compare commits
9 commits
783260b38c
...
8fc0ffa805
| Author | SHA1 | Date | |
|---|---|---|---|
|
8fc0ffa805 | ||
|
|
0ef7ebdad2 | ||
|
|
1d65b67260 | ||
|
|
04b2be8456 | ||
|
|
a56a8ffebc | ||
|
|
5f55e3ecee | ||
|
|
60da9bdb3f | ||
|
|
18481550d3 | ||
|
|
cea67b09ce |
5 changed files with 1898 additions and 492 deletions
|
|
@ -59,22 +59,26 @@ struct
|
|||
|
||||
(* value model & memory model *)
|
||||
|
||||
type deepvalue = ZeroDV
|
||||
| SmthDV
|
||||
| BotDV
|
||||
| FunDV of ((* data list * *) stmt) list
|
||||
| RefDV of deepvalue
|
||||
| TupleDV of deepvalue list
|
||||
(* type deepvalue = ZeroDV *)
|
||||
(* | SmthDV *)
|
||||
(* | BotDV *)
|
||||
(* | FunDV of ((* data list * *) stmt) list *)
|
||||
(* | RefDV of deepvalue *)
|
||||
(* | TupleDV of deepvalue list *)
|
||||
|
||||
type value = ZeroV
|
||||
| SmthV
|
||||
| BotV
|
||||
type memval = ZeroMV | SmthMV | BotMV (* | TopMV ?? *)
|
||||
type readval = ZeroRV | OneRV | TopRV
|
||||
type writeval = ZeroWV | SmthWV | OneWV
|
||||
|
||||
type value = UnitV of memval * readval * writeval
|
||||
| FunV of ((* data list * *) stmt) list
|
||||
| RefV of memid
|
||||
| TupleV of value list
|
||||
|
||||
type revpath = VarRP | DerefRP of revpath | AccessRP of revpath * data
|
||||
|
||||
type action = ReadA | AlwaysWriteA | MayWriteA
|
||||
|
||||
(* TODO: any additional difference between rvalue and lvalue now ?? *)
|
||||
|
||||
(* --- *)
|
||||
|
|
@ -138,16 +142,17 @@ struct
|
|||
let mem_set (mem : mem) (id : memid) (v : value) : mem =
|
||||
(list_replace (fst mem) (snd mem - id - 1) v, snd mem)
|
||||
|
||||
let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with
|
||||
| ZeroV -> ZeroDV
|
||||
| SmthV -> SmthDV
|
||||
| BotV -> BotDV
|
||||
| FunV s -> FunDV s
|
||||
| RefV id -> RefDV (v_to_deepv mem @@ mem_get mem id)
|
||||
| TupleV vs -> TupleDV (List.map (v_to_deepv mem) vs)
|
||||
(* let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with *)
|
||||
(* | ZeroV -> ZeroDV *)
|
||||
(* | SmthV -> SmthDV *)
|
||||
(* | BotV -> BotDV *)
|
||||
(* | FunV s -> FunDV s *)
|
||||
(* | RefV id -> RefDV (v_to_deepv mem @@ mem_get mem id) *)
|
||||
(* | TupleV vs -> TupleDV (List.map (v_to_deepv mem) vs) *)
|
||||
|
||||
let is_trivial_v (v : value) : bool =
|
||||
v == ZeroV || v == SmthV || v == BotV
|
||||
match v with | UnitV (_, _, _) -> true
|
||||
| _ -> false
|
||||
|
||||
(* --- path accessors --- *)
|
||||
|
||||
|
|
@ -191,22 +196,12 @@ struct
|
|||
(* - value construction *)
|
||||
|
||||
let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value =
|
||||
if is_trivial_v v
|
||||
then match t with
|
||||
| UnitT (Rd, _) -> (mem, v)
|
||||
| UnitT (NRd, _) -> (mem, BotV)
|
||||
| _ -> raise @@ Typing_error "valcopy: trivial value, wrong type"
|
||||
else match t, v with
|
||||
(* NOTE: replaced with if | best choice ?? *)
|
||||
(* | UnitT (Rd, w), ZeroV -> (mem, v) *)
|
||||
(* | UnitT (Rd, w), SmthV -> (mem, v) *)
|
||||
(* | UnitT (Rd, w), BotV -> (mem, v) *)
|
||||
(* | UnitT (NRd, w), ZeroV -> (mem, BotV) *)
|
||||
(* | UnitT (NRd, w), SmthV -> (mem, BotV) *)
|
||||
(* | UnitT (NRd, w), BotV -> (mem, BotV) *)
|
||||
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 (Cp, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in
|
||||
(* | 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 (mem, vs') v t -> let (mem', v') = valcopy mem v t in
|
||||
|
|
@ -215,24 +210,75 @@ struct
|
|||
(mem', TupleV (List.rev vs')) (* TODO: FIXME: should reverse or not ?? *)
|
||||
| _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type"
|
||||
|
||||
(* - action rules *)
|
||||
|
||||
let memvmod (a : action) (v_m : memval) : memval =
|
||||
match a, v_m with
|
||||
| ReadA, ZeroMV -> ZeroMV
|
||||
| ReadA, _ -> raise @@ Eval_error "memvmod: forbidden read"
|
||||
| AlwaysWriteA, _ -> ZeroMV
|
||||
| MayWriteA, ZeroMV -> ZeroMV
|
||||
| MayWriteA, _ -> SmthMV
|
||||
|
||||
let readvmod (a : action) (v_r : readval) : readval =
|
||||
match a, v_r with
|
||||
| _, TopRV -> TopRV
|
||||
| _, OneRV -> OneRV
|
||||
| ReadA, ZeroRV -> OneRV
|
||||
| AlwaysWriteA, ZeroRV -> TopRV
|
||||
| MayWriteA, ZeroRV -> ZeroRV
|
||||
|
||||
let writevmod (a : action) (v_w : writeval) : writeval =
|
||||
match a, v_w with
|
||||
| ReadA, v -> v
|
||||
| AlwaysWriteA, _ -> OneWV
|
||||
| MayWriteA, OneWV -> OneWV
|
||||
| MayWriteA, v -> v
|
||||
|
||||
(* - value update *)
|
||||
|
||||
let rec valupd (mem : mem) (v : value) (p : revpath) (b : value) : mem * value = match p, v with
|
||||
let rec valchange (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
|
||||
| DerefRP p, RefV id -> let (mem', v') = valchange 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"; *)
|
||||
| AccessRP (p, id), TupleV vs -> let (mem', v') = valchange mem (List.nth vs id) p b in
|
||||
(mem', TupleV (list_replace vs id v'))
|
||||
| _, _ -> raise @@ Typing_error "valupd"
|
||||
|
||||
let rec valupd (mem : mem) (v : value) (p : revpath) (a : action) : mem * value = match p, v with
|
||||
| VarRP, UnitV (v_m, v_r, v_w) -> (mem, UnitV (memvmod a v_m, readvmod a v_r, writevmod a v_w))
|
||||
| DerefRP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p a in
|
||||
(mem_set mem' id v', RefV id)
|
||||
| AccessRP (p, id), TupleV vs -> let (mem', v') = valupd mem (List.nth vs id) p a in
|
||||
(mem', TupleV (list_replace vs id v'))
|
||||
| _, _ -> raise @@ Typing_error "valupd"
|
||||
|
||||
(* - value combination *)
|
||||
|
||||
let memvalcomb (u : memval) (v : memval) : memval =
|
||||
match u, v with
|
||||
| ZeroMV, ZeroMV -> ZeroMV
|
||||
| BotMV, BotMV -> BotMV
|
||||
| _, _ -> SmthMV
|
||||
|
||||
let readvalcomb (u : readval) (v : readval) : readval =
|
||||
match u, v with
|
||||
| TopRV, TopRV -> TopRV
|
||||
| ZeroRV, ZeroRV -> ZeroRV
|
||||
| TopRV, ZeroRV -> ZeroRV
|
||||
| ZeroRV, TopRV -> ZeroRV
|
||||
| _, _ -> OneRV
|
||||
|
||||
let writevalcomb (u : writeval) (v : writeval) : writeval =
|
||||
match u, v with
|
||||
| OneWV, OneWV -> OneWV
|
||||
| ZeroWV, ZeroWV -> ZeroWV
|
||||
| _, _ -> SmthWV
|
||||
|
||||
let rec valcomb (u : value) (v : value) : value =
|
||||
if is_trivial_v u && is_trivial_v v
|
||||
then (if u == v then u else BotV)
|
||||
else match u, v with
|
||||
match u, v with
|
||||
| UnitV (u_m, u_r, u_w), UnitV (v_m, v_r, v_w) ->
|
||||
UnitV (memvalcomb u_m v_m, readvalcomb u_r v_r, writevalcomb u_w v_w)
|
||||
| FunV ustmts, FunV vstmts -> FunV (ustmts @ vstmts)
|
||||
| RefV a, RefV b -> if a == b then u else raise @@ Typing_error "valcomb: ref"
|
||||
| TupleV us, TupleV vs -> TupleV (List.map2 valcomb us vs)
|
||||
|
|
@ -246,7 +292,7 @@ struct
|
|||
(* - expression evaluation *)
|
||||
|
||||
let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with
|
||||
| UnitE -> ZeroV
|
||||
| UnitE -> UnitV (ZeroMV, ZeroRV, ZeroWV)
|
||||
| PathE p -> pathval mem vals p
|
||||
| RefE x -> RefV (vals_assoc x vals)
|
||||
| TupleE es -> TupleV (List.map (exprval mem vals) es)
|
||||
|
|
@ -287,48 +333,64 @@ struct
|
|||
|
||||
(* - call values spoil *)
|
||||
|
||||
(* TODO: check all cases *)
|
||||
let is_correct_tags (v : value) (r : read_cap) (w : write_cap)
|
||||
(r' : read_cap) (w' : write_cap) (m : mode)
|
||||
(c : copy_cap) : bool =
|
||||
(* FIXME TMP *)
|
||||
(* Printf.printf "%b %b %b %b %b\n" *)
|
||||
(* (r != Rd || v == ZeroV) *)
|
||||
(* (r != Rd || fst m == In) *)
|
||||
(* (snd m != Out || w == AlwaysWr) *)
|
||||
(* (* TODO: FIXME: why always write ?? *) *)
|
||||
(* (((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr)) *)
|
||||
(* (is_trivial_v v); *)
|
||||
(r != Rd || v == ZeroV) &&
|
||||
(r != Rd || fst m == In) &&
|
||||
(* TODO: check assignment type matches types separately later ?? *)
|
||||
let is_correct_tags (r : read_cap) (w : write_cap)
|
||||
(m : mode) (c : copy_cap) : bool =
|
||||
(snd m != Out || c == Rf) &&
|
||||
(snd m != Out || w == AlwaysWr) &&
|
||||
(* TODO: FIXME: check *)
|
||||
((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr) &&
|
||||
is_trivial_v v
|
||||
(r != Rd || fst m == In)
|
||||
|
||||
let tryread (r : read_cap) (v_m : memval)
|
||||
(v_r : readval) (v_w : writeval) : value =
|
||||
match r with
|
||||
| Rd -> UnitV (memvmod ReadA v_m,
|
||||
readvmod ReadA v_r,
|
||||
writevmod ReadA v_w)
|
||||
| NRd -> UnitV (v_m, v_r, v_w)
|
||||
|
||||
let tryspoil (m : mode) (w : write_cap) (v_m : memval) : memval =
|
||||
match m, w with
|
||||
| (_, 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)
|
||||
(u : atype) (m : mode) (c : copy_cap)
|
||||
: mem * value = match t, u, v with
|
||||
| UnitT (r, w), UnitT (r', w'), _ ->
|
||||
if not @@ is_trivial_v v
|
||||
then raise @@ Typing_error "valspoil: unit, not trivial"
|
||||
else if not @@ is_correct_tags v r w r' w' m c
|
||||
then raise @@ Typing_error "valspoil: unit, not correct"
|
||||
else if snd m == NOut && c == Rf && (w == AlwaysWr || w == MayWr)
|
||||
then (mem, BotV)
|
||||
else if snd m == Out && w == AlwaysWr
|
||||
then (mem, ZeroV)
|
||||
else (mem, v)
|
||||
| FunT ts, FunT us, FunV _ -> if ts == us then (mem, v) else raise @@ Typing_error "valspoil: fun"
|
||||
| RefT (ct, t), RefT (cu, u), RefV id ->
|
||||
let (mem', v') = valspoil mem (mem_get mem id) t u m ct in
|
||||
(m : mode) (c : copy_cap)
|
||||
: mem * value = match t, v with
|
||||
| UnitT (r, w), UnitV (v_m, v_r, v_w) ->
|
||||
if not @@ is_correct_tags r w m c
|
||||
then raise @@ Typing_error "valspoil: trivial type tags combination is not correct"
|
||||
else
|
||||
let v' = tryread r v_m v_r v_w in
|
||||
if c == Cp || w == NeverWr
|
||||
then (mem, v')
|
||||
else (match v' with
|
||||
| UnitV (v_m', v_r', v_w') ->
|
||||
let (v_m'', v_r'', v_w'') =
|
||||
(if w == AlwaysWr
|
||||
then (memvmod AlwaysWriteA v_m',
|
||||
readvmod AlwaysWriteA v_r',
|
||||
writevmod AlwaysWriteA 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''))
|
||||
| _ -> raise @@ Typing_error "valspoil: value after tryread is not unit")
|
||||
| FunT ts, FunV _ -> (mem, v)
|
||||
| RefT (ct, t), RefV id ->
|
||||
let (mem', v') = valspoil mem (mem_get mem id) t m ct in
|
||||
(mem_set mem id v', RefV id)
|
||||
| TupleT ts, TupleT us, TupleV vs ->
|
||||
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', vs') = list_foldl3 folder (mem, []) ts us vs in
|
||||
| TupleT ts, TupleV vs ->
|
||||
let folder = fun (mem, vs') t v ->
|
||||
let (mem', v') = valspoil mem v t m c in (mem', v' :: vs') in
|
||||
let (mem', vs') = List.fold_left2 folder (mem, []) ts vs in
|
||||
(mem', TupleV (List.rev vs'))
|
||||
| _, _, _ -> raise @@ Typing_error "valspoil"
|
||||
| _, _ -> raise @@ Typing_error "valspoil"
|
||||
|
||||
(* full spoil *)
|
||||
|
||||
|
|
@ -337,11 +399,11 @@ struct
|
|||
let x = pathvar p in
|
||||
let id = vals_assoc x vals in (* base var address *)
|
||||
let b = pathval mem vals p in (* subvalue in var *)
|
||||
let t' = pathtype types p in (* type of subvalue *)
|
||||
let (mem', b') = valspoil mem b t t' m Cp in (* spoil subvalue *)
|
||||
(* let t' = pathtype types p in (* type of subvalue *) *)
|
||||
let (mem', b') = valspoil mem b t m Cp in (* spoil subvalue *)
|
||||
(* TODO: FIXME: why copy (Cp)? maybe sometimes use top-level capability ? *)
|
||||
let pi = pathrev p VarRP in
|
||||
let (mem'', v'') = valupd mem' (mem_get mem' id) pi b' in (* set subvalue into var *)
|
||||
let (mem'', v'') = valchange 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 =
|
||||
|
|
@ -369,15 +431,34 @@ struct
|
|||
(* NOTE: not needed due to performed optimization in stmt_eval *)
|
||||
(* let func_eval (mem : mem) (vals : vals) (s : stmt) (ts : mtype list) (es : expr list) = *)
|
||||
|
||||
let writeval_to_cap (v_w : writeval) : write_cap =
|
||||
match v_w with
|
||||
| ZeroWV -> NeverWr
|
||||
| SmthWV -> MayWr
|
||||
| OneWV -> AlwaysWr
|
||||
|
||||
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) ->
|
||||
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"
|
||||
|
||||
(* - statement evaluation *)
|
||||
|
||||
let rec stmt_eval (state : state) (s : stmt) : state =
|
||||
match state with (mem, types, vals, visited) -> match s with
|
||||
| SkipS -> state
|
||||
| CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *)
|
||||
pathval mem vals f in
|
||||
let t = (* FIXME TMP Printf.printf "call, before t\n"; *)
|
||||
pathtype types f in
|
||||
| CallS (f, es) -> let v = pathval mem vals f in
|
||||
let t = pathtype types f in
|
||||
let types' : types = (fst types, fst types) in
|
||||
let vals' : vals = (fst vals, fst vals) in
|
||||
(match v, t with
|
||||
|
|
@ -394,7 +475,14 @@ struct
|
|||
if List.mem stmt visited_old
|
||||
then stmt :: visited_old
|
||||
else match stmt_eval (mem_swa, types_swa, vals_swa, stmt :: visited_old) stmt with
|
||||
(_, _, _, visited_after_stmt) -> visited_after_stmt)
|
||||
(mem_after_stmt, _, vals_after_stmt, visited_after_stmt) ->
|
||||
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
|
||||
tags_check mem_after_stmt v t; x + 1)
|
||||
0 ts;
|
||||
visited_after_stmt)
|
||||
visited_swa
|
||||
fstmts in
|
||||
let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *)
|
||||
|
|
@ -412,16 +500,28 @@ struct
|
|||
else let x = pathvar p in
|
||||
let id = vals_assoc x vals in
|
||||
let pi = pathrev p VarRP in
|
||||
let (mem', v') = valupd mem (mem_get mem id) pi ZeroV in
|
||||
let (mem', v') = valupd mem (mem_get mem id) pi AlwaysWriteA in
|
||||
(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")
|
||||
| ReadS p -> if pathval mem vals p == SmthV || pathval mem vals p == BotV
|
||||
then raise @@ Eval_error "read: spoiled value"
|
||||
else if pathval mem vals p != ZeroV
|
||||
then raise @@ Eval_error "read: nontrivial value"
|
||||
else state
|
||||
| ReadS p -> (match pathtype types p with
|
||||
| UnitT (_, _) ->
|
||||
(* NOTE: not required *)
|
||||
(* if r == NRd *)
|
||||
(* then raise @@ Eval_error "read: not read tag" *)
|
||||
(* else *)
|
||||
let x = pathvar p in
|
||||
let id = vals_assoc x vals in
|
||||
let pi = pathrev p VarRP in
|
||||
let (mem', v') = valupd mem (mem_get mem id) pi ReadA in
|
||||
(mem_set mem' id v', types, vals, visited)
|
||||
| RefT _ -> raise @@ Eval_error "read: ref type"
|
||||
| TupleT _ -> raise @@ Eval_error "read: tuple type"
|
||||
| _ -> raise @@ Eval_error "read: type")
|
||||
(* NOTE: handled inside through undefined in memvmod *)
|
||||
(* if pathval mem vals p == SmthV || pathval mem vals p == BotV *)
|
||||
(* then raise @@ Eval_error "read: spoiled value" *)
|
||||
| SeqS (sl, sr) -> let statel = stmt_eval state sl in
|
||||
stmt_eval statel sr
|
||||
| ChoiceS (sl, sr) -> let statel = stmt_eval state sl in
|
||||
|
|
@ -470,6 +570,7 @@ struct
|
|||
let vg8 = VarP (globals_min_id + 8)
|
||||
let vg9 = VarP (globals_min_id + 9)
|
||||
let vg10 = VarP (globals_min_id + 10)
|
||||
let vg11 = VarP (globals_min_id + 11)
|
||||
|
||||
let rf0E = RefE 0
|
||||
let rf1E = RefE 1
|
||||
|
|
@ -518,23 +619,30 @@ struct
|
|||
let rdS p = ReadS p
|
||||
let callS f args = CallS (f, args)
|
||||
|
||||
let uV m = UnitV (m, ZeroRV, ZeroWV)
|
||||
|
||||
(* - utils tests *)
|
||||
|
||||
let v_memval_is v m =
|
||||
match v with
|
||||
| UnitV (v_m, _, _) -> v_m == m
|
||||
| _ -> false
|
||||
|
||||
let%expect_test "mem add / get / set" =
|
||||
let mem = empty_mem in
|
||||
let (mem, id1) = mem_add mem ZeroV in
|
||||
let (mem, id2) = mem_add mem SmthV in
|
||||
let (mem, id3) = mem_add mem BotV in
|
||||
let (mem, id1) = mem_add mem @@ uV ZeroMV in
|
||||
let (mem, id2) = mem_add mem @@ uV SmthMV in
|
||||
let (mem, id3) = mem_add mem @@ uV BotMV in
|
||||
Printf.printf "%i %i %i " id1 id2 id3;
|
||||
Printf.printf "%b %b %b " (mem_get mem id1 == ZeroV)
|
||||
(mem_get mem id2 == SmthV)
|
||||
(mem_get mem id3 == BotV);
|
||||
let mem = mem_set mem id1 BotV in
|
||||
let mem = mem_set mem id2 ZeroV in
|
||||
let mem = mem_set mem id3 SmthV in
|
||||
Printf.printf "%b %b %b" (mem_get mem id1 == BotV)
|
||||
(mem_get mem id2 == ZeroV)
|
||||
(mem_get mem id3 == SmthV);
|
||||
Printf.printf "%b %b %b " (v_memval_is (mem_get mem id1) ZeroMV)
|
||||
(v_memval_is (mem_get mem id2) SmthMV)
|
||||
(v_memval_is (mem_get mem id3) BotMV);
|
||||
let mem = mem_set mem id1 @@ uV BotMV in
|
||||
let mem = mem_set mem id2 @@ uV ZeroMV in
|
||||
let mem = mem_set mem id3 @@ uV SmthMV in
|
||||
Printf.printf "%b %b %b" (v_memval_is (mem_get mem id1) BotMV)
|
||||
(v_memval_is (mem_get mem id2) ZeroMV)
|
||||
(v_memval_is (mem_get mem id3) SmthMV);
|
||||
[%expect {| 0 1 2 true true true true true true |}]
|
||||
|
||||
(* - basic var tests *)
|
||||
|
|
@ -555,7 +663,7 @@ struct
|
|||
ReadS (VarP globals_min_id));
|
||||
[%expect.unreachable]);
|
||||
with Eval_error msg -> Printf.printf "%s" msg;
|
||||
[%expect {| read: spoiled value |}]
|
||||
[%expect {| memvmod: forbidden read |}]
|
||||
|
||||
let%expect_test "simple vars, no read & read" =
|
||||
prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE);
|
||||
|
|
@ -621,10 +729,10 @@ struct
|
|||
let%expect_test "simple call with write, dsl" =
|
||||
prog_eval_noret (
|
||||
[
|
||||
defgu uT_r_mw;
|
||||
defg (rfT uT_r_mw) rfg0E;
|
||||
defgu uT_aw;
|
||||
defg (rfT uT_aw) rfg0E;
|
||||
FunD (
|
||||
[moded @@ cpT @@ uT_r_mw],
|
||||
[moded @@ cpT @@ uT_aw],
|
||||
wrS @@ drf @@ v0
|
||||
)
|
||||
],
|
||||
|
|
@ -636,10 +744,10 @@ struct
|
|||
let%expect_test "simple call with read after write, dsl" =
|
||||
prog_eval_noret (
|
||||
[
|
||||
defgu uT_r_mw;
|
||||
defg (rfT uT_r_mw) rfg0E;
|
||||
defgu uT_aw;
|
||||
defg (rfT uT_aw) rfg0E;
|
||||
FunD (
|
||||
[moded @@ cpT @@ uT_mw],
|
||||
[moded @@ cpT @@ uT_aw],
|
||||
(wrS @@ drf @@ v0) #.
|
||||
(rdS @@ drf @@ v0)
|
||||
)
|
||||
|
|
@ -696,7 +804,7 @@ struct
|
|||
);
|
||||
[%expect.unreachable]);
|
||||
with Eval_error msg -> Printf.printf "%s" msg;
|
||||
[%expect {| read: spoiled value |}]
|
||||
[%expect {| memvmod: forbidden read |}]
|
||||
|
||||
let%expect_test "simple call with write to ref with fix, dsl" =
|
||||
prog_eval_noret (
|
||||
|
|
@ -779,9 +887,9 @@ struct
|
|||
prog_eval_noret (
|
||||
[
|
||||
defgu uT_r_aw;
|
||||
defg (rfT uT_r_aw) rfg0E;
|
||||
defg (rfT uT_r) rfg0E;
|
||||
FunD (
|
||||
[moded @@ cpT @@ uT_aw],
|
||||
[moded @@ cpT @@ uT],
|
||||
(wrS @@ vg0) #.
|
||||
(rdS @@ drf @@ vg1)
|
||||
)
|
||||
|
|
@ -795,10 +903,10 @@ struct
|
|||
let%expect_test "simple call with read & write (2 args), dsl" =
|
||||
prog_eval_noret (
|
||||
[
|
||||
defgu uT_r_aw;
|
||||
defg (rfT uT_r_aw) rfg0E;
|
||||
defgu uT_r_aw;
|
||||
defg (rfT uT_r_aw) rfg2E;
|
||||
defgu uT_r;
|
||||
defg (rfT uT_r) rfg0E;
|
||||
defgu uT_aw;
|
||||
defg (rfT uT_aw) rfg2E;
|
||||
FunD (
|
||||
[
|
||||
moded @@ rfT @@ uT_r;
|
||||
|
|
@ -826,10 +934,10 @@ struct
|
|||
defg (rfT uT_r_aw) rfg6E;
|
||||
FunD (
|
||||
[
|
||||
((NIn, NOut), cpT @@ uT_aw);
|
||||
((NIn, NOut), cpT @@ uT);
|
||||
((In, NOut), cpT @@ uT_r_aw);
|
||||
((NIn, Out), cpT @@ uT_aw);
|
||||
((In, Out), cpT @@ uT_r_aw);
|
||||
((NIn, Out), rfT @@ uT_aw);
|
||||
((In, Out), rfT @@ uT_r_aw);
|
||||
],
|
||||
(rdS @@ drf @@ v1) #.
|
||||
(rdS @@ drf @@ v3) #.
|
||||
|
|
@ -850,10 +958,10 @@ struct
|
|||
let%expect_test "simple call with different arguments modifiers, ref, dsl" =
|
||||
prog_eval_noret (
|
||||
[
|
||||
defgu uT_r_aw;
|
||||
defg (rfT uT_r_aw) rfg0E;
|
||||
defgu uT_r_aw;
|
||||
defg (rfT uT_r_aw) rfg2E;
|
||||
defgu uT_r;
|
||||
defg (rfT uT_r) rfg0E;
|
||||
defgu uT_r;
|
||||
defg (rfT uT_r) rfg2E;
|
||||
defgu uT_r_aw;
|
||||
defg (rfT uT_r_aw) rfg4E;
|
||||
defgu uT_r_aw;
|
||||
|
|
@ -880,83 +988,195 @@ struct
|
|||
Printf.printf "done!";
|
||||
[%expect {| done! |}]
|
||||
|
||||
(* - complex tests *)
|
||||
(* - tests for presentation *)
|
||||
|
||||
(* NOTE: path access isreversed to intuitive function application
|
||||
by definition *)
|
||||
let%expect_test "complex test: send, dsl" =
|
||||
let%expect_test "presentation test 1 (simple types), 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;
|
||||
defgu uT_r_aw;
|
||||
defg requestT requestE;
|
||||
get_version_idF;
|
||||
updated_versionF;
|
||||
sendF;
|
||||
send_allF
|
||||
defg (rfT uT_r_aw) rfg0E; (* x *)
|
||||
defgu uT_r_aw;
|
||||
defg (rfT uT_r_aw) rfg2E; (* y *)
|
||||
defgu uT_r_aw;
|
||||
defg (rfT uT_r_aw) rfg4E; (* z *)
|
||||
defgu uT_r_aw;
|
||||
defg (rfT uT_r_aw) rfg6E; (* k *)
|
||||
FunD ( (* f *)
|
||||
[
|
||||
(moded @@ rfT @@ uT_r_aw);
|
||||
(moded @@ rfT @@ uT_r);
|
||||
],
|
||||
callS send_allID [pE varID]
|
||||
(rdS @@ drf @@ v0) #.
|
||||
(wrS @@ drf @@ v0) #.
|
||||
(rdS @@ drf @@ v1)
|
||||
);
|
||||
FunD ( (* w *)
|
||||
[
|
||||
(moded @@ cpT @@ uT_mw);
|
||||
],
|
||||
(wrS @@ drf @@ v0) |. skp
|
||||
);
|
||||
FunD ( (* g *)
|
||||
[
|
||||
(moded @@ rfT @@ uT_aw);
|
||||
(moded @@ cpT @@ uT_r_mw);
|
||||
],
|
||||
(wrS @@ drf @@ v0) #.
|
||||
((wrS @@ drf @@ v1) |. (wrS @@ drf @@ v0)) #.
|
||||
(rdS @@ drf @@ v0) #.
|
||||
(rdS @@ drf @@ v1)
|
||||
);
|
||||
FunD ( (* r *)
|
||||
[
|
||||
(moded @@ rfT @@ uT_r);
|
||||
],
|
||||
(rdS @@ drf @@ v0)
|
||||
)
|
||||
],
|
||||
let xV = vg1 in
|
||||
let yV = vg3 in
|
||||
let zV = vg5 in
|
||||
let kV = vg7 in
|
||||
let fF = vg8 in
|
||||
let wF = vg9 in
|
||||
let gF = vg10 in
|
||||
let rF = vg11 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])
|
||||
);
|
||||
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; *)
|
||||
(* defgu 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; *)
|
||||
(* defgu 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
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@
|
|||
|
||||
== Syntax
|
||||
|
||||
*TODO: top-level value copy mode ??* // TODO: FIXME
|
||||
// *TODO: top-level value copy mode ??* // TODO: FIXME
|
||||
|
||||
*TODO: add formal global env to all types and vals (as in code) ??* // TODO: FIXME
|
||||
|
||||
|
|
@ -48,6 +48,9 @@
|
|||
#let cl = $chevron.l$
|
||||
#let cr = $chevron.r$
|
||||
|
||||
#let cdl = $chevron.l.double$
|
||||
#let cdr = $chevron.r.double$
|
||||
|
||||
#let expr = `expr`
|
||||
#let stmt = `stmt`
|
||||
#let decl = `decl`
|
||||
|
|
@ -151,55 +154,73 @@
|
|||
|
||||
== Value Model
|
||||
|
||||
#let deepValue = `deepvalue`
|
||||
// #let deepValue = `deepvalue`
|
||||
#let value = `value`
|
||||
#let vmem = $v_#[`mem`]$
|
||||
#let vread = $v_#[`read`]$
|
||||
#let vwrite = $v_#[`write`]$
|
||||
#let revpath = $#[`path`]_#[`rev`]$
|
||||
|
||||
#bnf(
|
||||
// Prod(
|
||||
// $deepValue$,
|
||||
// {
|
||||
// Or[$0$][valid value of simple type] // `Unit`
|
||||
// Or[$\#$][valid or spoiled value of simple type] // `Unit`
|
||||
// Or[$bot$][spoiled value of simple type] // `Unit`
|
||||
// Or[$lambda space (X+ stmt)+$][function pointer value, set of possible values] // `Fun`
|
||||
// Or[$rf deepValue$][reference value, contains label of the value in the memory] // `Ref`
|
||||
// Or[$[deepValue+]$][tuple value] // `Prod`
|
||||
// }
|
||||
// ),
|
||||
Prod(
|
||||
$deepValue$,
|
||||
$vmem$,
|
||||
{
|
||||
Or[$0$][valid value of simple type] // `Unit`
|
||||
Or[$\#$][valid or spoiled value of simple type] // `Unit`
|
||||
Or[$bot$][spoiled value of simple type] // `Unit`
|
||||
Or[$lambda space (X+ stmt)+$][function pointer value, set of possible values] // `Fun`
|
||||
Or[$rf deepValue$][reference value, contains label of the value in the memory] // `Ref`
|
||||
Or[$[deepValue+]$][tuple value] // `Prod`
|
||||
Or[$0$][valid value of simple type]
|
||||
Or[$?$][valid or spoiled value of simple type]
|
||||
Or[$bot$][spoiled value of simple type]
|
||||
// NOTE: proably can't use correctly
|
||||
// Or[$top$][value that is not spoiled because of the copy tag]
|
||||
}
|
||||
),
|
||||
Prod(
|
||||
$vread$,
|
||||
{
|
||||
Or[$0_r$][argument not read]
|
||||
Or[$1_r$][argument read]
|
||||
Or[$top_r$][argument already written from the function beginning]
|
||||
}
|
||||
),
|
||||
Prod(
|
||||
$vwrite$,
|
||||
{
|
||||
Or[$0_w$][no write]
|
||||
Or[$?_w$][maybe write]
|
||||
Or[$1_w$][always write]
|
||||
}
|
||||
),
|
||||
Prod(
|
||||
$value_mu$,
|
||||
{
|
||||
Or[$0$][valid value of simple type] // `Unit`
|
||||
Or[$\#$][valid or spoiled value of simple type] // `Unit`
|
||||
Or[$bot$][spoiled value of simple type] // `Unit`
|
||||
Or[$cdl vmem, vread, vwrite cdr$][value of the simple type, contains cells for analysis] // `Unit`
|
||||
Or[$lambda space (X+ stmt)+$][function pointer value, set of possible values] // `Fun`
|
||||
Or[$rf LL$][reference value, contains label of the value in the memory] // `Ref`
|
||||
Or[$[value+]$][tuple value] // `Prod`
|
||||
}
|
||||
),
|
||||
Prod(
|
||||
revpath,
|
||||
{
|
||||
Or[$\# .$][value by itself]
|
||||
Or[$rf revpath$][reference to value]
|
||||
Or[$n . revpath$][tuple with value as $n$-th element]
|
||||
}
|
||||
),
|
||||
)
|
||||
|
||||
#deepValue - полное значение, #value - слой значения, привязан к конкретной памяти $mu$
|
||||
// #deepValue - полное значение,
|
||||
#value - слой значения, привязан к конкретной памяти $mu$
|
||||
|
||||
Значения, могут лежать в переменных и передаваться как аргументы функций (то, во что вычисляется $expr$)
|
||||
|
||||
$revpath$ - путь в обратную сторону, используется для обновления значений
|
||||
|
||||
$v in value$ - произвольное значение
|
||||
|
||||
Получение #deepValue по #value:
|
||||
- $rf l xarrowSquiggly(mu)_#[deep] rf mu[l]$
|
||||
- $* xarrowSquiggly(mu)_#[deep] *$
|
||||
где $*$ - произвольный конструктор значения, кроме $rf$
|
||||
// Получение #deepValue по #value:
|
||||
// - $rf l xarrowSquiggly(mu)_#[deep] rf mu[l]$
|
||||
// - $* xarrowSquiggly(mu)_#[deep] *$
|
||||
// где $*$ - произвольный конструктор значения, кроме $rf$
|
||||
|
||||
== Memory Model
|
||||
|
||||
|
|
@ -223,13 +244,44 @@ $v in value$ - произвольное значение
|
|||
|
||||
== Semantics
|
||||
|
||||
#let action = `action`
|
||||
#let readA = $#[`READ`]_a$
|
||||
#let writeA = $#[`WRITE`]_a$
|
||||
#let mbwriteA = $#[`MAYWRITE`]_a$
|
||||
// #let spoilA = $#[`SPOIL`]_a$
|
||||
// #let nospoilA = $#[`NOSPOIL`]_a$
|
||||
|
||||
#bnf(
|
||||
Prod(
|
||||
revpath,
|
||||
{
|
||||
Or[$\# .$][value by itself]
|
||||
Or[$rf revpath$][reference to value]
|
||||
Or[$n . revpath$][tuple with value as $n$-th element]
|
||||
}
|
||||
),
|
||||
Prod(
|
||||
$action$,
|
||||
{
|
||||
Or[$readA$][value read]
|
||||
Or[$writeA$][value written]
|
||||
Or[$mbwriteA$][value maybe written]
|
||||
// NOTE: not required, spoils only first element ?
|
||||
// Or[$spoilA$][value passed as funciton argument and spoiled]
|
||||
// NOTE: probably acutally can't reliebly forbid Cp
|
||||
// Or[$nospoilA$][value passed as funciton argument and not changed,
|
||||
// but could be spoiled if mode will be $Copy$ instead of $Ref$]
|
||||
// TODO: better wording ??
|
||||
}
|
||||
),
|
||||
)
|
||||
|
||||
// TODO: FIXME: add vars & funcs from global context in the beginnning
|
||||
|
||||
// $V := memelem$ - значения памяти
|
||||
|
||||
$X$ - можество переменных
|
||||
|
||||
|
||||
#let vals = $Sigma$
|
||||
#let types = $Gamma$
|
||||
#let envv = $#[env]_Sigma$
|
||||
|
|
@ -237,6 +289,11 @@ $X$ - можество переменных
|
|||
$sigma : envv := X -> LL, space vals : envv$ - #[ метки памяти перменных контекста, частично определённая функция ]
|
||||
$sigma : envt := X -> type, space types : envt$ - #[ типы значений перменных контекста, частично определённая функция ]
|
||||
|
||||
$revpath$ - путь в обратную сторону, используется для обновления значений
|
||||
|
||||
$action$ - действия, совершаемые с примитивным значением,
|
||||
модифицирующие содержащуюся таминформацию
|
||||
|
||||
// $DD : X -> decl$ - глобальные определения, частично определённая функция
|
||||
|
||||
// $d in decl, $
|
||||
|
|
@ -437,7 +494,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
|||
// // $sigma temode x -> cr r' space w' cl$, // NOTE: not required, value passed
|
||||
// $(w = AlwaysWrite or w = MaybeWrite) and (m = (\_, Out) or c = Ref) => w' = AlwaysWrite$,
|
||||
// // $sigma, mu teval x eqmu v$, // NOTE: not required, value passed
|
||||
// $v in {0, \#, bot}$,
|
||||
// $v in {0, ?, bot}$,
|
||||
// $r = Read => v = 0$,
|
||||
// $types, vals, mu, m, c tcorrect v : cl r', w' cr -> cl r, w cr$,
|
||||
// )
|
||||
|
|
@ -485,18 +542,33 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
|||
rule(
|
||||
name: [ new trivial read value],
|
||||
|
||||
$v in {0, \#, bot}$,
|
||||
$cl v, mu cr xarrowSquiggly(cl Read \, w cr)_new cl v, mu cr$,
|
||||
$v_m in {0, ?, bot}$,
|
||||
$cl cdl v_m, v_r, v_w cdr, mu cr
|
||||
xarrowSquiggly(cl Read \, w cr)_new
|
||||
cl cdl v_m, 0, 0 cdr, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ new trivial read $top$ value],
|
||||
|
||||
// $cl cdl top, v_r, v_w cdr, mu cr
|
||||
// xarrowSquiggly(cl Read \, w cr)_new
|
||||
// cl cdl 0, 0, 0 cdr, mu cr$,
|
||||
// )
|
||||
// ))
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ new trivial $not$ read value],
|
||||
|
||||
$v in {0, \#, bot}$,
|
||||
$cl v, mu cr xarrowSquiggly(cl not Read \, w cr)_new cl bot, mu cr$,
|
||||
$v_m in {0, ?, bot/*, top */}$,
|
||||
$cl cdl v_m, v_r, v_w cdr, mu cr
|
||||
xarrowSquiggly(cl not Read \, w cr)_new
|
||||
cl cdl bot, 0, 0 cdr, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -505,32 +577,30 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
|||
rule(
|
||||
name: [ new funciton pointer value],
|
||||
|
||||
$cl lambda overline(t) s, mu cr xarrowSquiggly(lambda space c space overline(t))_new cl lambda overline(t) s, mu cr$,
|
||||
$cl lambda overline(s), mu cr xarrowSquiggly(lambda space c space overline(t))_new cl lambda overline(s), mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ new reference ref value],
|
||||
|
||||
// $cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$,
|
||||
// )
|
||||
// ))
|
||||
|
||||
// NOTE: due to new memory cells types (with rw subcells) valnue should always be copied
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ new reference ref value],
|
||||
|
||||
// TODO: FIXME: recursive copy ?? (what heppens if ref field has copy substructure ??)
|
||||
// <- forbidden ??
|
||||
|
||||
$cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ new reference copy value],
|
||||
name: [ new reference /* copy */ value],
|
||||
|
||||
$cl mu[l], mu cr xarrowSquiggly(t)_new cl v, mu_v cr$,
|
||||
|
||||
$mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$,
|
||||
|
||||
$cl rf l, mu cr xarrowSquiggly(rf Copy t)_new cl rf l', mu_a cr$,
|
||||
$cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_new cl rf l', mu_a cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -547,18 +617,108 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
|||
)
|
||||
))
|
||||
|
||||
=== Action Rules
|
||||
|
||||
#let modM = $attach(<-, br: m)$
|
||||
#let modR = $attach(<-, br: r)$
|
||||
#let modW = $attach(<-, br: w)$
|
||||
|
||||
#align(center, grid(
|
||||
columns: 3,
|
||||
gutter: 10%,
|
||||
align: center,
|
||||
table(
|
||||
columns: 3,
|
||||
table.header(
|
||||
[*a*], [*x*], $modM$
|
||||
),
|
||||
$readA$, $0$, $0$,
|
||||
// $readA$, $top$, $0$,
|
||||
$readA$, $?$, $-$, // err
|
||||
$readA$, $bot$, $-$, // err
|
||||
$writeA$, $0$, $0$,
|
||||
// $writeA$, $top$, $-$,
|
||||
$writeA$, $?$, $0$,
|
||||
$writeA$, $bot$, $0$,
|
||||
$mbwriteA$, $0$, $0$,
|
||||
// $mbwriteA$, $top$, $top$,
|
||||
$mbwriteA$, $?$, $?$,
|
||||
$mbwriteA$, $bot$, $?$,
|
||||
// $spoilA$, $0$, $bot$,
|
||||
// // $spoilA$, $top$, $bot$,
|
||||
// $spoilA$, $?$, $bot$,
|
||||
// $spoilA$, $bot$, $bot$,
|
||||
// $nospoilA$, $0$, $top$,
|
||||
// $nospoilA$, $top$, $top$,
|
||||
// $nospoilA$, $?$, $-$, // ??
|
||||
// $nospoilA$, $bot$, $-$,
|
||||
),
|
||||
|
||||
table(
|
||||
columns: 3,
|
||||
table.header(
|
||||
[*a*], [*x*], $modR$
|
||||
),
|
||||
$readA$, $1$, $1$,
|
||||
$readA$, $0$, $1$,
|
||||
$readA$, $top$, $top$,
|
||||
$writeA$, $1$, $1$,
|
||||
$writeA$, $0$, $top$,
|
||||
$writeA$, $top$, $top$,
|
||||
$mbwriteA$, $1$, $1$,
|
||||
$mbwriteA$, $0$, $0$,
|
||||
$mbwriteA$, $top$, $top$,
|
||||
|
||||
// $spoilA$, $1$, $1$,
|
||||
// $spoilA$, $0$, $0$,
|
||||
// $spoilA$, $top$, $top$,
|
||||
// $nospoilA$, $1$, $1$,
|
||||
// $nospoilA$, $0$, $0$,
|
||||
// $nospoilA$, $top$, $top$,
|
||||
),
|
||||
|
||||
table(
|
||||
columns: 3,
|
||||
table.header(
|
||||
[*a*], [*x*], $modW$
|
||||
),
|
||||
$readA$, $1$, $1$,
|
||||
$readA$, $?$, $?$,
|
||||
$readA$, $0$, $0$,
|
||||
$writeA$, $1$, $1$,
|
||||
$writeA$, $?$, $1$,
|
||||
$writeA$, $0$, $1$,
|
||||
$mbwriteA$, $1$, $1$,
|
||||
$mbwriteA$, $?$, $?$,
|
||||
$mbwriteA$, $0$, $?$,
|
||||
|
||||
// $spoilA$, $1$, $1$,
|
||||
// $spoilA$, $?$, $?$,
|
||||
// $spoilA$, $0$, $0$,
|
||||
// $nospoilA$, $1$, $1$,
|
||||
// $nospoilA$, $?$, $?$,
|
||||
// $nospoilA$, $0$, $0$,
|
||||
)
|
||||
))
|
||||
|
||||
Прочерк \"$-$\" означает, что данная операция не определена.
|
||||
|
||||
=== Value Update
|
||||
|
||||
#let modify = `modify`
|
||||
==== Change
|
||||
|
||||
Замена подзначения в значении по $revpath$, $b in value$.
|
||||
|
||||
#let change = `change`
|
||||
|
||||
// TODO: add type check ??
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ modify end value],
|
||||
name: [ change final value],
|
||||
|
||||
// $v in {0, \#, bot}$,
|
||||
$cl v, mu cr xarrowSquiggly(cl \# . \, b cr)_modify cl b, mu cr$,
|
||||
// $v in {0, ?, bot}$,
|
||||
$cl v, mu cr xarrowSquiggly(cl \# . \, b cr)_change cl b, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -567,10 +727,54 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
|||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ new reference copy value],
|
||||
name: [ change reference value],
|
||||
|
||||
$cl mu[l], mu cr xarrowSquiggly(cl pi \, b cr)_modify cl v', mu' cr$,
|
||||
$cl rf l, mu cr xarrowSquiggly(cl rf pi \, b cr)_modify cl rf l, mu'[l <- v'] cr$,
|
||||
$cl mu[l], mu cr xarrowSquiggly(cl pi \, b cr)_change cl v', mu' cr$,
|
||||
$cl rf l, mu cr xarrowSquiggly(cl rf pi \, b cr)_change cl rf l, mu'[l <- v'] cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ change tuple value],
|
||||
|
||||
$cl v_i, mu cr xarrowSquiggly(cl p \, b cr)_change cl v'_i, mu', cr$,
|
||||
$cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl i.pi \, b cr)_change cl [v_1, ... v'_i, ... v_n], mu' cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
==== Modify
|
||||
|
||||
Совершение операции над тривиальным подзначением в значении по $revpath$, $a in action$
|
||||
|
||||
#let modify = `modify`
|
||||
|
||||
// TODO: add type check ??
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ modify final value],
|
||||
|
||||
$cl cdl v_m, v_r, v_w cdr, mu cr
|
||||
xarrowSquiggly(cl \# . \, a cr)_modify
|
||||
cl cdl v_m modM a, v_r modR a, v_w modW a cdr, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ modify reference value],
|
||||
|
||||
$cl mu[l], mu cr xarrowSquiggly(cl pi \, a cr)_modify cl v', mu' cr$,
|
||||
$cl rf l, mu cr xarrowSquiggly(cl rf pi \, a cr)_modify cl rf l, mu'[l <- v'] cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -581,8 +785,8 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
|||
rule(
|
||||
name: [ modify tuple value],
|
||||
|
||||
$cl v_i, mu cr xarrowSquiggly(cl p \, b cr)_modify cl v'_i, mu', cr$,
|
||||
$cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl i.pi \, b cr)_modify cl [v_1, ... v'_i, ... v_n], mu' cr$,
|
||||
$cl v_i, mu cr xarrowSquiggly(cl p \, a cr)_modify cl v'_i, mu', cr$,
|
||||
$cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl i.pi \, a cr)_modify cl [v_1, ... v'_i, ... v_n], mu' cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -590,29 +794,74 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
|||
|
||||
=== Value Combination
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ combine same trivial values],
|
||||
#align(center, grid(
|
||||
columns: 3,
|
||||
gutter: 20%,
|
||||
align: center,
|
||||
table(
|
||||
columns: 3,
|
||||
table.header(
|
||||
[*x*], [*y*], $plus.o_m$
|
||||
),
|
||||
$0$, $0$, $0$,
|
||||
// $0$, $top$, $0$,
|
||||
$0$, $?$, $?$,
|
||||
$0$, $bot$, $?$,
|
||||
$?$, $0$, $?$,
|
||||
$?$, $?$, $?$,
|
||||
$?$, $bot$, $?$,
|
||||
// $?$, $top$, $?$,
|
||||
$bot$, $0$, $?$,
|
||||
$bot$, $?$, $?$,
|
||||
// $bot$, $top$, $?$,
|
||||
// $top$, $0$, $?$,
|
||||
// $top$, $?$, $?$,
|
||||
// $top$, $bot$, $?$,
|
||||
$bot$, $bot$, $bot$,
|
||||
// $top$, $top$, $top$,
|
||||
),
|
||||
|
||||
$v_1 in {0, \#, bot}$,
|
||||
$v_2 in {0, \#, bot}$,
|
||||
$v_1 = v_2$,
|
||||
$v_1 plus.o v_2 = v_1$
|
||||
table(
|
||||
columns: 3,
|
||||
table.header(
|
||||
[*x*], [*y*], $plus.o_r$
|
||||
),
|
||||
$1$, $1$, $1$,
|
||||
$1$, $0$, $1$,
|
||||
$1$, $top$, $1$,
|
||||
$0$, $1$, $1$,
|
||||
$top$, $1$, $1$,
|
||||
$0$, $0$, $0$,
|
||||
$0$, $top$, $0$,
|
||||
$top$, $0$, $0$,
|
||||
$top$, $top$, $top$,
|
||||
),
|
||||
|
||||
table(
|
||||
columns: 3,
|
||||
table.header(
|
||||
[*x*], [*y*], $plus.o_w$
|
||||
),
|
||||
$1$, $1$, $1$,
|
||||
$1$, $?$, $?$,
|
||||
$1$, $0$, $?$,
|
||||
$?$, $1$, $?$,
|
||||
$?$, $?$, $?$,
|
||||
$?$, $0$, $?$,
|
||||
$0$, $1$, $?$,
|
||||
$0$, $?$, $?$,
|
||||
$0$, $0$, $0$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ combine different trivial values],
|
||||
name: [ combine trivial values],
|
||||
|
||||
$v_1 in {0, \#, bot}$,
|
||||
$v_2 in {0, \#, bot}$,
|
||||
$v_1 != v_2$,
|
||||
$v_1 plus.o v_2 = \#$
|
||||
$v_1 = cdl v_1_m, v_1_r, v_1_w cdr$,
|
||||
$v_2 = cdl v_2_m, v_2_r, v_2_w cdr$,
|
||||
$v_1 plus.o v_2 = cdl v_1_m plus.o_m v_2_m, v_1_r plus.o_r v_2_r, v_1_w plus.o_w v_2_w cdr$
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -691,7 +940,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
|||
rule(
|
||||
name: [ unit expr value],
|
||||
|
||||
$vals, mu texpre () eqmu 0$,
|
||||
$vals, mu texpre () eqmu cdl 0_m, 0_r, 0_w cdr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -812,37 +1061,20 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
|||
=== Call Values Spoil
|
||||
|
||||
#let spoil = `spoil`
|
||||
#let tryread = `try read`
|
||||
#let tryspoil = `try spoil`
|
||||
|
||||
// TODO: FIXME: complete rule check
|
||||
#let tcorrectnew = $attach(tack.r.double, br: #[correct])$
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ correctness],
|
||||
|
||||
$r = Read => v = 0$,
|
||||
$r = Read => m = (In, \_)$,
|
||||
$m = (\_, Out) => c = Ref$,
|
||||
$m = (\_, Out) => w = AlwaysWrite$,
|
||||
$(w = AlwaysWrite or w = MaybeWrite) and (m = (\_, Out) or c = Ref) => w' = AlwaysWrite$,
|
||||
$r = Read => m = (In, \_)$,
|
||||
|
||||
$v in {0, \#, bot}$,
|
||||
|
||||
$ tcorrectnew cl v, r, w, r', w', m, c cr $,
|
||||
)
|
||||
))
|
||||
|
||||
// TODO: extract correctness
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ spoil step],
|
||||
|
||||
$ tcorrectnew cl v, r, w, r', w', m, c cr $,
|
||||
|
||||
$w = AlwaysWrite or w = MaybeWrite$,
|
||||
$v in {0, \#, bot}$,
|
||||
$cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \, (\_, not Out) \, not Copy)_spoil cl bot, mu cr$,
|
||||
$ tcorrectnew cl r, w, m, c cr $,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -851,13 +1083,103 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
|||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ fix step],
|
||||
name: [ argument read],
|
||||
|
||||
$ tcorrectnew cl v, r, w, r', w', m, c cr $,
|
||||
$cl v_m, v_r, v_w cr,
|
||||
xarrowSquiggly(Read)_tryread
|
||||
cl v_m modW readA, v_r modR readA, v_w modW readA cr$,
|
||||
)
|
||||
))
|
||||
|
||||
$w = AlwaysWrite$,
|
||||
$v in {0, \#, bot}$,
|
||||
$cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \, (\_, Out) \, c)_spoil cl 0, mu cr$,
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ argument not read],
|
||||
|
||||
$cl v_m, v_r, v_w cr,
|
||||
xarrowSquiggly(not Read)_tryread
|
||||
cl v_m, v_r, v_w cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ value maybe spoiled],
|
||||
|
||||
$v_m,
|
||||
xarrowSquiggly(not Out \, MaybeWrite)_tryspoil
|
||||
?$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ value always spoiled],
|
||||
|
||||
$v_m,
|
||||
xarrowSquiggly(not Out \, AlwaysWrite)_tryspoil
|
||||
bot$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ value not spoiled],
|
||||
|
||||
$v_m,
|
||||
xarrowSquiggly(Out \, w)_tryspoil
|
||||
v_m$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ write spoil step],
|
||||
|
||||
$ tcorrectnew cl r, w, m, c cr $,
|
||||
$cl v_m, v_r, v_w cr,
|
||||
xarrowSquiggly(r)_tryread
|
||||
cl v_m', v_r', v_w' cr$,
|
||||
|
||||
$v_m' modW writeA xarrowSquiggly(o \, AlwaysWrite)_tryspoil v_m''$,
|
||||
|
||||
$cl cdl v_m, v_r, v_w cdr, mu cr
|
||||
xarrowSquiggly(cl r \, AlwaysWrite cr \, (\_, o) \, Ref)_spoil
|
||||
cl cdl v_m'', v_r' modR writeA, v_w' modW writeA cdr, cdr, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ maybe write step],
|
||||
|
||||
$ tcorrectnew cl r, w, m, c cr $,
|
||||
$cl v_m, v_r, v_w cr,
|
||||
xarrowSquiggly(r)_tryread
|
||||
cl v_m', v_r', v_w' cr$,
|
||||
|
||||
$v_m' modW mbwriteA xarrowSquiggly(o \, MaybeWrite)_tryspoil v_m''$,
|
||||
|
||||
$cl cdl v_m, v_r, v_w cdr, mu cr
|
||||
xarrowSquiggly(cl r \, MaybeWrite cr \, (\_, o) \, Ref)_spoil
|
||||
cl cdl v_m'', v_r' modR mbwriteA, v_w' modW mbwriteA cdr, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -868,12 +1190,16 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
|||
rule(
|
||||
name: [ skip step],
|
||||
|
||||
$ tcorrectnew cl v, r, w, r', w', m, c cr $,
|
||||
$ tcorrectnew cl r, w, m, c cr $,
|
||||
$cl v_m, v_r, v_w cr,
|
||||
xarrowSquiggly(r)_tryread
|
||||
cl v_m', v_r', v_w' cr$,
|
||||
|
||||
$not "spoil step"$,
|
||||
$not "fix step"$,
|
||||
$v in {0, \#, bot}$,
|
||||
$cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \, (\_, not Out) \, c)_spoil cl v, mu cr$,
|
||||
$c = Copy or w = NotWrite$,
|
||||
|
||||
$cl cdl v_m, v_r, v_w cdr, mu cr
|
||||
xarrowSquiggly(cl r \, w cr cr \, (\_, \_) \, c)_spoil
|
||||
cl cdl v_m', v_r', v_w' cdr mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -945,7 +1271,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
|||
// FIXME depends on parent ??
|
||||
$cl b, mu cr xarrowSquiggly(t \, t' \, m \, Copy)_spoil cl b', mu' cr$,
|
||||
$p arrrevpath^(\#.) pi$,
|
||||
$cl mu'[l], mu' cr xarrowSquiggly(cl pi \, b' cr)_modify cl v'', mu'' cr$,
|
||||
$cl mu'[l], mu' cr xarrowSquiggly(cl pi \, b' cr)_change cl v'', mu'' cr$,
|
||||
|
||||
$mu stretch(=>)^(m space t space p)_(cl vals, types cr) mu''[l <- v'']$,
|
||||
)
|
||||
|
|
@ -1009,6 +1335,80 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
|||
|
||||
=== Function Evaluation
|
||||
|
||||
#align(center, grid(
|
||||
columns: 2,
|
||||
gutter: 20%,
|
||||
align: center,
|
||||
|
||||
[
|
||||
$ x ~_r t$
|
||||
|
||||
#table(
|
||||
columns: 2,
|
||||
table.header(
|
||||
[*x*], [*t*]
|
||||
),
|
||||
$1$, $Read$,
|
||||
$0$, $not Read$,
|
||||
$top$, $not Read$,
|
||||
)
|
||||
],
|
||||
|
||||
[
|
||||
$x ~_w t$
|
||||
#table(
|
||||
columns: 2,
|
||||
table.header(
|
||||
[*x*], [*t*]
|
||||
),
|
||||
$0$, $NotWrite$,
|
||||
$?$, $MaybeWrite$,
|
||||
$1$, $AlwaysWrite$,
|
||||
)
|
||||
]
|
||||
))
|
||||
|
||||
#let ttags = $attach(tack.r, br: #[`tags`])$
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ trivial type check],
|
||||
|
||||
$v_r ~_r r$,
|
||||
$v_w ~_w w$,
|
||||
$mu ttags cdl v_m, v_r, v_w cdr : cl r, w cr$,
|
||||
)
|
||||
))
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ lambda check],
|
||||
|
||||
$mu ttags lambda space overline(s) :$,
|
||||
)
|
||||
))
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ reference check],
|
||||
|
||||
$mu ttags mu[l] : t$,
|
||||
$mu ttags rf l : rf t$,
|
||||
)
|
||||
))
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ tuple check],
|
||||
|
||||
$mu ttags v_1 : t_1$,
|
||||
$...$,
|
||||
$mu ttags v_n : t_n$,
|
||||
$mu ttags [v_1, ... v_n] : [t_1, ... t_n]$,
|
||||
)
|
||||
))
|
||||
|
||||
#let tfunceval = $attach(tack.r.double, br: #[func eval])$
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
|
|
@ -1028,10 +1428,16 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
|||
xarrowDashed(x_n space t_n space e_n)_vals
|
||||
cl types_n, vals_n, mu_n cr$,
|
||||
|
||||
// NOTE: eval function body
|
||||
$cl types_n, vals_n, mu_n cr
|
||||
xarrow(s)
|
||||
cl types', vals', mu' cr$,
|
||||
|
||||
// NOTE: check that read and write tags are used properly
|
||||
$mu' ttags mu'[vals'[x_1]] : t_1$,
|
||||
$...$,
|
||||
$mu' ttags mu'[vals'[x_n]] : t_n$,
|
||||
|
||||
$vals, mu_0 tfunceval cl s, [x_1, .. x_n], [t_1, ... t_n], [e_1, ... e_n] cr$,
|
||||
)
|
||||
))
|
||||
|
|
@ -1066,7 +1472,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
|||
$...$,
|
||||
$vals, mu_0 tfunceval cl s_n, overline(x)_n, [t_1, ... t_n], [e_1, ... e_n] cr$,
|
||||
|
||||
// NOTE: thick arrow to "spoil" context
|
||||
// NOTE: "spoil" context for each argument usage
|
||||
$mu_0 stretch(=>)^(m_1 space t_1 space e_1)_(cl vals, types cr) mu_1$,
|
||||
$...$,
|
||||
$mu_(n - 1) stretch(=>)^(m_n space t_n space e_n)_(cl vals, types cr) mu_n$,
|
||||
|
|
@ -1089,7 +1495,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
|||
$p arrpath x$,
|
||||
$l = vals[x]$,
|
||||
$p arrrevpath^(\#.) pi$,
|
||||
$mu[l] xarrowSquiggly(cl pi \, 0 cr)_modify v'$,
|
||||
$mu[l] xarrowSquiggly(cl pi \, writeA cr)_modify v'$,
|
||||
|
||||
$cl types, vals, mu cr
|
||||
xarrow("WRITE" p)
|
||||
|
|
@ -1102,18 +1508,25 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
|
|||
rule(
|
||||
name: [ READ $p$],
|
||||
|
||||
$vals, mu tval p eqmu 0$,
|
||||
// TODO: already handled in modify ?
|
||||
// $vals, mu tval p eqmu cdr v_m, \_, \_ cdl$,
|
||||
// $v_m in { 0, top }$,
|
||||
|
||||
$types ttype p : cl r, w cr$,
|
||||
$r = Read$,
|
||||
$p arrpath x$,
|
||||
$l = vals[x]$,
|
||||
$p arrrevpath^(\#.) pi$,
|
||||
$mu[l] xarrowSquiggly(cl pi \, readA cr)_modify v'$,
|
||||
|
||||
$cl types, vals, mu cr
|
||||
xarrow("READ" p)
|
||||
cl types, vals, mu cr$,
|
||||
cl types, vals, mu[l <- v'] cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
|
|
|
|||
|
|
@ -164,12 +164,44 @@ struct
|
|||
|
||||
(* NOTE: deepvalue - not used (?) *)
|
||||
|
||||
module MemVal = struct
|
||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
||||
[%%ocanren_inject
|
||||
type nonrec t = ZeroMV | SmthMV | BotMV
|
||||
[@@deriving gt ~options:{ show; gmap }]
|
||||
type ground = t
|
||||
]
|
||||
end
|
||||
|
||||
module ReadVal = struct
|
||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
||||
[%%ocanren_inject
|
||||
type nonrec t = ZeroRV | OneRV | TopRV
|
||||
[@@deriving gt ~options:{ show; gmap }]
|
||||
type ground = t
|
||||
]
|
||||
end
|
||||
|
||||
module WriteVal = struct
|
||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
||||
[%%ocanren_inject
|
||||
type nonrec t = ZeroWV | SmthWV | OneWV
|
||||
[@@deriving gt ~options:{ show; gmap }]
|
||||
type ground = t
|
||||
]
|
||||
end
|
||||
|
||||
module Value = struct
|
||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
||||
[%%ocanren_inject
|
||||
type nonrec ('sl, 'd, 'vl) t = ZeroV | SmthV | BotV | FunV of 'sl | RefV of 'd | TupleV of 'vl
|
||||
type nonrec ('vm, 'vr, 'vw, 'sl, 'd, 'vl) t = UnitV of 'vm * 'vr * 'vw
|
||||
| FunV of 'sl
|
||||
| RefV of 'd
|
||||
| TupleV of 'vl
|
||||
[@@deriving gt ~options:{ show; gmap }]
|
||||
type ground = (((* Nat.ground List.ground * *) Stmt.ground) List.ground, Nat.ground, ground List.ground) t
|
||||
type ground = (MemVal.ground, ReadVal.ground, WriteVal.ground,
|
||||
((* Nat.ground List.ground * *) Stmt.ground) List.ground,
|
||||
Nat.ground, ground List.ground) t
|
||||
]
|
||||
end
|
||||
|
||||
|
|
@ -182,6 +214,15 @@ struct
|
|||
]
|
||||
end
|
||||
|
||||
module Action = struct
|
||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
||||
[%%ocanren_inject
|
||||
type nonrec t = ReadA | AlwaysWriteA | MayWriteA
|
||||
[@@deriving gt ~options:{ show; gmap }]
|
||||
type ground = t
|
||||
]
|
||||
end
|
||||
|
||||
(* --- *)
|
||||
|
||||
module MemEnv = struct
|
||||
|
|
@ -340,6 +381,17 @@ struct
|
|||
{ xs == [] & ys == [] & zs == [] }
|
||||
}
|
||||
|
||||
(* NOTE: unrequired ? *)
|
||||
(* let list_map2o f xs ys zs = ocanren { *)
|
||||
(* { xs == [] & ys == [] } | *)
|
||||
(* { fresh x', xs', y', ys', z', zs' in *)
|
||||
(* xs == x' :: xs' & *)
|
||||
(* ys == y' :: ys' & *)
|
||||
(* f x' y' z' *)
|
||||
(* mapo f xs' ys' zs' & *)
|
||||
(* zs == z' :: zs' } *)
|
||||
(* } *)
|
||||
|
||||
(* - state utils *)
|
||||
|
||||
let types_assoco id types tp =
|
||||
|
|
@ -459,7 +511,8 @@ struct
|
|||
let is_trivial_vo v =
|
||||
let open Value in
|
||||
ocanren {
|
||||
v == ZeroV | v == SmthV | v == BotV
|
||||
fresh v_m, v_r, v_w in
|
||||
v == UnitV (v_m, v_r, v_w)
|
||||
}
|
||||
|
||||
let rec pathvaro p x =
|
||||
|
|
@ -516,11 +569,11 @@ struct
|
|||
pathvalo mem vals p' v' &
|
||||
v' == RefV id &
|
||||
mem_geto mem id v } |
|
||||
{ fresh p', id, v', vs in
|
||||
p == AccessP (p', id) &
|
||||
{ fresh p', id', v', vs in
|
||||
p == AccessP (p', id') &
|
||||
pathvalo mem vals p' v' &
|
||||
v' == TupleV vs &
|
||||
list_ntho vs id v }
|
||||
list_ntho vs id' v }
|
||||
}
|
||||
|
||||
(* --- eval rules --- *)
|
||||
|
|
@ -539,13 +592,20 @@ struct
|
|||
let open Type in
|
||||
let open Value in
|
||||
let open ReadCap in
|
||||
let open CopyCap in
|
||||
(* let open CopyCap in *)
|
||||
let open MemVal in
|
||||
let open ReadVal in
|
||||
let open WriteVal in
|
||||
ocanren {
|
||||
{ fresh r, w in
|
||||
is_trivial_vo v &
|
||||
tp == UnitT (r, w) &
|
||||
{ { r == Rd & mem_with_id' == Std.pair mem v } |
|
||||
{ r == NRd & mem_with_id' == Std.pair mem BotV } } } |
|
||||
{ { fresh v_m, _v_r, _v_w in
|
||||
r == Rd &
|
||||
v == UnitV (v_m, _v_r, _v_w) &
|
||||
mem_with_id' == Std.pair mem (UnitV (v_m, ZeroRV, ZeroWV)) } |
|
||||
{ r == NRd &
|
||||
mem_with_id' == Std.pair mem (UnitV (BotMV, ZeroRV, ZeroWV)) } } } |
|
||||
{ fresh stmts, ts in
|
||||
v == FunV stmts &
|
||||
tp == FunT ts &
|
||||
|
|
@ -553,13 +613,13 @@ struct
|
|||
{ fresh c, tp', id in
|
||||
v == RefV id &
|
||||
tp == RefT (c, tp') &
|
||||
{ { c == Rf & mem_with_id' == Std.pair mem v } |
|
||||
(* { c == Rf & mem_with_id' == Std.pair mem v } | *)
|
||||
{ fresh v', mem_cp, v_cp, mem_add, id_add in
|
||||
c == Cp &
|
||||
(* c == Cp & *)
|
||||
mem_geto mem id v' &
|
||||
valcopyo mem v' tp' (Std.pair mem_cp v_cp) &
|
||||
mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
|
||||
mem_with_id' == (mem_add, RefV id_add) } } } |
|
||||
mem_with_id' == (mem_add, RefV id_add) } } |
|
||||
{ fresh vs, tps, mem', vs' in
|
||||
v == TupleV vs &
|
||||
tp == TupleT tps &
|
||||
|
|
@ -567,10 +627,43 @@ struct
|
|||
mem_with_id' == Std.pair mem' (TupleV vs') }
|
||||
}
|
||||
|
||||
(* - action rules *)
|
||||
|
||||
let memvmodo a v_m v_m' =
|
||||
let open MemVal in
|
||||
let open Action in
|
||||
ocanren {
|
||||
{ a == ReadA & v_m == ZeroMV & v_m' == ZeroMV } |
|
||||
{ a == AlwaysWriteA & v_m' == ZeroMV } |
|
||||
{ a == MayWriteA & v_m == ZeroMV & v_m' == ZeroMV } |
|
||||
{ a == MayWriteA & v_m =/= ZeroMV & v_m' == SmthMV }
|
||||
}
|
||||
|
||||
let readvmodo a v_r v_r' =
|
||||
let open ReadVal in
|
||||
let open Action in
|
||||
ocanren {
|
||||
{ v_r == TopRV & v_r' == TopRV } |
|
||||
{ v_r == OneRV & v_r' == OneRV } |
|
||||
{ a == ReadA & v_r == ZeroRV & v_r' == OneRV } |
|
||||
{ a == AlwaysWriteA & v_r == ZeroRV & v_r' == TopRV } |
|
||||
{ a == MayWriteA & v_r == ZeroRV & v_r' == ZeroRV }
|
||||
}
|
||||
|
||||
let writevmodo a v_w v_w' =
|
||||
let open WriteVal in
|
||||
let open Action in
|
||||
ocanren {
|
||||
{ a == ReadA & v_w' == v_w } |
|
||||
{ a == AlwaysWriteA & v_w' == OneWV } |
|
||||
{ a == MayWriteA & v_w == OneWV & v_w' == OneWV } |
|
||||
{ a == MayWriteA & v_w =/= OneWV & v_w' == v_w }
|
||||
}
|
||||
|
||||
(* - value update *)
|
||||
|
||||
(* NOTE: reversed path used *)
|
||||
let rec valupdo mem v rp b mem_with_v' =
|
||||
let rec valchangeo mem v rp b mem_with_v' =
|
||||
let open RevPath in
|
||||
let open Value in
|
||||
ocanren {
|
||||
|
|
@ -580,7 +673,7 @@ struct
|
|||
rp == DerefRP rp' &
|
||||
v == RefV id &
|
||||
mem_geto mem id v' &
|
||||
valupdo mem v' rp' b mem_with_v_upd &
|
||||
valchangeo 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) } |
|
||||
|
|
@ -588,7 +681,40 @@ struct
|
|||
rp == AccessRP (rp', id) &
|
||||
v == TupleV vs' &
|
||||
list_ntho vs' id v' &
|
||||
valupdo mem v' rp' b mem_with_v_upd &
|
||||
valchangeo 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) }
|
||||
}
|
||||
|
||||
(* NOTE: reversed path used *)
|
||||
let rec valupdo mem v rp a mem_with_v' =
|
||||
let open RevPath in
|
||||
let open Value in
|
||||
ocanren {
|
||||
{ fresh v_m, v_r, v_w,
|
||||
v_m', v_r', v_w',
|
||||
v' in
|
||||
rp == VarRP &
|
||||
v == UnitV (v_m, v_r, v_w) &
|
||||
memvmodo a v_m v_m' &
|
||||
readvmodo a v_r v_r' &
|
||||
writevmodo a v_w v_w' &
|
||||
v' == UnitV (v_m', v_r', v_w') &
|
||||
mem_with_v' == Std.pair mem v' } |
|
||||
{ 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' rp' a 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 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' rp' a 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) }
|
||||
|
|
@ -596,13 +722,50 @@ struct
|
|||
|
||||
(* - value combination *)
|
||||
|
||||
let memvalcombo u v u' =
|
||||
let open MemVal in
|
||||
ocanren {
|
||||
{ u == ZeroMV & v == ZeroMV & u' == ZeroMV } |
|
||||
{ u == BotMV & v == BotMV & u' == BotMV } |
|
||||
{ { u =/= ZeroMV | { u == ZeroMV & v =/= ZeroMV } } &
|
||||
{ u =/= BotMV | { u == BotMV & v =/= BotMV } } &
|
||||
u' == SmthMV }
|
||||
}
|
||||
|
||||
let readvalcombo u v u' =
|
||||
let open ReadVal in
|
||||
ocanren {
|
||||
{ u == TopRV & v == TopRV & u' == TopRV } |
|
||||
{ u == ZeroRV & v == ZeroRV & u' == ZeroRV } |
|
||||
{ u == TopRV & v == ZeroRV & u' == ZeroRV } |
|
||||
{ u == ZeroRV & v == TopRV & u' == ZeroRV } |
|
||||
{ u =/= TopRV & v =/= TopRV &
|
||||
u =/= ZeroRV & v =/= ZeroRV &
|
||||
u' == OneRV }
|
||||
}
|
||||
|
||||
let writevalcombo u v u' =
|
||||
let open WriteVal in
|
||||
ocanren {
|
||||
{ u == OneWV & v == OneWV & u' == OneWV } |
|
||||
{ u == ZeroWV & v == ZeroWV & u' == ZeroWV } |
|
||||
{ { u =/= ZeroWV | { u == ZeroWV & v =/= ZeroWV } } &
|
||||
{ u =/= OneWV | { u == OneWV & v =/= OneWV } } &
|
||||
u' == SmthWV }
|
||||
}
|
||||
|
||||
let rec valcombo u v u' =
|
||||
let open Value in
|
||||
ocanren {
|
||||
{ is_trivial_vo u &
|
||||
is_trivial_vo v &
|
||||
(* TODO: do not use disequality constraint ? *)
|
||||
{ { u == v & u' == u } | { u =/= v & u' == BotV } } } |
|
||||
{ fresh u_m, u_r, u_w,
|
||||
v_m, v_r, v_w,
|
||||
u_m', u_r', u_w' in
|
||||
u == UnitV (u_m, u_r, u_w) &
|
||||
v == UnitV (v_m, v_r, v_w) &
|
||||
memvalcombo u_m v_m u_m' &
|
||||
readvalcombo u_r v_r u_r' &
|
||||
writevalcombo u_w v_w u_w' &
|
||||
u' == UnitV (u_m', u_r', u_w') } |
|
||||
{ fresh ustmts, vstmts, ustmts' in
|
||||
u == FunV ustmts &
|
||||
v == FunV vstmts &
|
||||
|
|
@ -612,7 +775,8 @@ struct
|
|||
{ fresh a, b in
|
||||
u == RefV a &
|
||||
v == RefV b &
|
||||
a == b } |
|
||||
a == b &
|
||||
u' == RefV a } |
|
||||
{ fresh us, vs, us' in
|
||||
u == TupleV us &
|
||||
v == TupleV vs &
|
||||
|
|
@ -642,8 +806,11 @@ struct
|
|||
exprvalo mem vals e v' =
|
||||
let open Expr in
|
||||
let open Value in
|
||||
let open MemVal in
|
||||
let open ReadVal in
|
||||
let open WriteVal in
|
||||
ocanren {
|
||||
{ e == UnitE & v' == ZeroV } |
|
||||
{ e == UnitE & v' == UnitV (ZeroMV, ZeroRV, ZeroWV) } |
|
||||
{ fresh p in
|
||||
e == PathE p &
|
||||
pathvalo mem vals p v' } |
|
||||
|
|
@ -698,7 +865,6 @@ struct
|
|||
types', vals' in
|
||||
d == VarD (tp, e) &
|
||||
exprvalo mem vals e v &
|
||||
(* v == TupleV [ZeroV; ZeroV] & (* FIXME TMP *) *)
|
||||
valcopyo mem v tp (Pair.pair mem_cp v_cp) &
|
||||
(* mem_cp == mem & v_cp == v & *)
|
||||
mem_addo mem_cp v_cp (Pair.pair mem_add id_add) &
|
||||
|
|
@ -760,76 +926,100 @@ struct
|
|||
(* - call values spoil *)
|
||||
|
||||
(* TODO: check that negation is interpreted correctly *)
|
||||
let is_correct_tagso v r w _r' w' m c =
|
||||
let open Value in
|
||||
let is_correct_tagso r w m c =
|
||||
let open ReadCap in
|
||||
let open WriteCap in
|
||||
let open Mode in
|
||||
let open CopyCap in
|
||||
ocanren {
|
||||
{ r == NRd | r == Rd & v == ZeroV } &
|
||||
{ r == NRd | r == Rd & is_ino m } &
|
||||
{ is_not_outo m | is_outo m & w == AlwaysWr } &
|
||||
{ w == NeverWr |
|
||||
w =/= NeverWr & w' =/= AlwaysWr & is_not_outo m & c == Cp |
|
||||
w =/= NeverWr & w' == AlwaysWr } &
|
||||
is_trivial_vo v
|
||||
{ is_not_outo m | is_outo m & w == AlwaysWr & c == Rf }
|
||||
}
|
||||
|
||||
let rec valspoil_foldero m c mem_with_vs tp u v mem_with_vs' = ocanren {
|
||||
fresh mem, vs, mem', v' in
|
||||
Std.pair mem vs == mem_with_vs &
|
||||
valspoilo mem v tp u m c (Std.pair mem' v') &
|
||||
mem_with_vs' == Std.pair mem' (v' :: vs)
|
||||
}
|
||||
and valspoilo mem v tp u m c mem_with_v' =
|
||||
let open Type in
|
||||
let tryreado r v_m v_r v_w v' =
|
||||
let open Action in
|
||||
let open Value in
|
||||
let open ReadCap in
|
||||
ocanren {
|
||||
{ fresh v_m', v_r', v_w' in
|
||||
r == Rd &
|
||||
memvmodo ReadA v_m v_m' &
|
||||
readvmodo ReadA v_r v_r' &
|
||||
writevmodo ReadA v_w v_w' &
|
||||
v' == UnitV (v_m', v_r', v_w') } |
|
||||
{ r == NRd &
|
||||
v' == UnitV (v_m, v_r, v_w)}
|
||||
}
|
||||
|
||||
let tryspoilo m w v_m v_m' =
|
||||
let open Mode in
|
||||
let open WriteCap in
|
||||
let open CopyCap in
|
||||
let open MemVal in
|
||||
ocanren {
|
||||
{ fresh r, w, r', w' in
|
||||
{ is_outo m & { w == AlwaysWr | w == MayWr } & v_m' == v_m } |
|
||||
{ is_not_outo m & w == AlwaysWr & v_m' == BotMV } |
|
||||
{ is_not_outo m & w == MayWr & v_m' == SmthMV }
|
||||
}
|
||||
|
||||
let rec valspoil_foldero m c mem_with_vs tp v mem_with_vs' = ocanren {
|
||||
fresh mem, vs, mem', v' in
|
||||
Std.pair mem vs == mem_with_vs &
|
||||
valspoilo mem v tp m c (Std.pair mem' v') &
|
||||
mem_with_vs' == Std.pair mem' (v' :: vs)
|
||||
}
|
||||
and valspoilo mem v tp m c mem_with_v' =
|
||||
let open Type in
|
||||
let open Value in
|
||||
let open WriteCap in
|
||||
let open CopyCap in
|
||||
let open Action in
|
||||
ocanren {
|
||||
{ fresh r, w,
|
||||
v_m, v_r, v_w,
|
||||
v', v'' in
|
||||
tp == UnitT (r, w) &
|
||||
u == UnitT (r', w') &
|
||||
is_trivial_vo v &
|
||||
is_correct_tagso v r w r' w' m c &
|
||||
v == UnitV (v_m, v_r, v_w) &
|
||||
is_correct_tagso r w m c &
|
||||
tryreado r v_m v_r v_w v' &
|
||||
{
|
||||
{ is_not_outo m &
|
||||
{ { c == Cp | { c == Rf & w == NeverWr } } &
|
||||
mem_with_v' == Std.pair mem v' } |
|
||||
{ fresh v_m', v_r', v_w',
|
||||
v_m'', v_r'', v_w'',
|
||||
v_m''' in
|
||||
c == Rf &
|
||||
{ w == AlwaysWr | w == MayWr } &
|
||||
mem_with_v' == Std.pair mem BotV } |
|
||||
{ is_outo m &
|
||||
w == AlwaysWr &
|
||||
mem_with_v' == Std.pair mem ZeroV } |
|
||||
{ { is_outo m |
|
||||
is_not_outo m & c == Cp |
|
||||
is_not_outo m & c == Rf & w == NeverWr } &
|
||||
{ is_not_outo m |
|
||||
is_outo m & w == MayWr |
|
||||
is_outo m & w == NeverWr } &
|
||||
mem_with_v' == Std.pair mem v }
|
||||
v' == UnitV (v_m', v_r', v_w') &
|
||||
{
|
||||
{ w == AlwaysWr &
|
||||
memvmodo AlwaysWriteA v_m' v_m'' &
|
||||
readvmodo AlwaysWriteA v_r' v_r'' &
|
||||
writevmodo AlwaysWriteA v_w' v_w'' } |
|
||||
{ w == MayWr &
|
||||
memvmodo MayWriteA v_m' v_m'' &
|
||||
readvmodo MayWriteA v_r' v_r'' &
|
||||
writevmodo MayWriteA v_w' v_w'' }
|
||||
} &
|
||||
tryspoilo m w v_m'' v_m''' &
|
||||
v'' == UnitV (v_m''', v_r'', v_w'') &
|
||||
mem_with_v' == Std.pair mem v'' }
|
||||
} } |
|
||||
{ fresh ts, us, _stmts in
|
||||
{ fresh ts, _stmts in
|
||||
tp == FunT ts &
|
||||
u == FunT us &
|
||||
v == FunV _stmts &
|
||||
ts == us &
|
||||
mem_with_v' == Std.pair mem v } |
|
||||
{ fresh ctp', tp', cu', u', id', v', mem_sp, v_sp, mem_set in
|
||||
{ fresh ctp', tp', id', v', mem_sp, v_sp, mem_set in
|
||||
tp == RefT (ctp', tp') &
|
||||
u == RefT (cu', u') &
|
||||
v == RefV id' &
|
||||
mem_geto mem id' v' &
|
||||
valspoilo mem v' tp' u' m ctp' (Std.pair mem_sp v_sp) &
|
||||
valspoilo mem v' tp' m ctp' (Std.pair mem_sp v_sp) &
|
||||
mem_seto mem_sp id' v_sp mem_set &
|
||||
mem_with_v' == Std.pair mem_set (RefV id') } |
|
||||
{ fresh tps, us, vs, mem_sp, vs_sp in
|
||||
{ fresh tps, vs, mem_sp, vs_sp in
|
||||
tp == TupleT tps &
|
||||
u == TupleT us &
|
||||
v == TupleV vs &
|
||||
list_foldr3o (valspoil_foldero m c)
|
||||
(Std.pair mem []) tps us vs
|
||||
list_foldr2o (valspoil_foldero m c)
|
||||
(Std.pair mem []) tps vs
|
||||
(Std.pair mem_sp vs_sp) &
|
||||
mem_with_v' == Std.pair mem_sp (TupleV vs_sp)
|
||||
}
|
||||
|
|
@ -837,34 +1027,34 @@ struct
|
|||
|
||||
(* full spoil *)
|
||||
|
||||
let argspoilpo st m tp p mem' =
|
||||
let argsspoilpo 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', rp,
|
||||
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 &
|
||||
vals_assoco x vals id &
|
||||
pathvalo mem vals p b &
|
||||
pathtypeo types p tp' &
|
||||
valspoilo mem b tp tp' m Cp (Std.pair mem_sp b_sp) &
|
||||
mem_geto mem_sp id v_sp &
|
||||
(* pathtypeo types p tp' & *)
|
||||
valspoilo mem b tp m Cp (Std.pair mem_sp b_sp) &
|
||||
pathrevo p VarRP rp &
|
||||
valupdo mem_sp v_sp rp b_sp (Std.pair mem_upd v_upd) &
|
||||
mem_geto mem_sp id v_sp &
|
||||
valchangeo mem_sp v_sp rp b_sp (Std.pair mem_upd v_upd) &
|
||||
mem_seto mem_upd id v_upd mem'
|
||||
}
|
||||
|
||||
let rec argspoile_foldero types vals visited m mem tp e mem' =
|
||||
let rec argsspoile_foldero types vals visited m mem tp e mem' =
|
||||
let open StEnv in
|
||||
ocanren {
|
||||
fresh st in
|
||||
st == StEnv (mem, types, vals, visited) &
|
||||
argspoileo st m tp e mem'
|
||||
argsspoileo st m tp e mem'
|
||||
}
|
||||
and argspoileo st m tp e mem' =
|
||||
and argsspoileo st m tp e mem' =
|
||||
let open StEnv in
|
||||
let open Expr in
|
||||
let open Type in
|
||||
|
|
@ -878,14 +1068,14 @@ struct
|
|||
mem' == mem } |
|
||||
{ fresh p in
|
||||
e == PathE p &
|
||||
argspoilpo st m tp p mem' } |
|
||||
argsspoilpo st m tp p mem' } |
|
||||
{ fresh x in
|
||||
e == RefE x &
|
||||
argspoilpo st m tp (VarP x) mem' } |
|
||||
argsspoilpo st m tp (VarP x) mem' } |
|
||||
{ fresh es, tps in
|
||||
e == TupleE es &
|
||||
tp == TupleT tps &
|
||||
list_foldl2o (argspoile_foldero types vals visited m) mem tps es mem'}
|
||||
list_foldl2o (argsspoile_foldero types vals visited m) mem tps es mem'}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -910,8 +1100,47 @@ struct
|
|||
(* - function evaluation *)
|
||||
(* NOTE: not needed due to performed optimization in stmt_eval ? *)
|
||||
|
||||
let writeval_to_capo v_w w' =
|
||||
let open WriteVal in
|
||||
let open WriteCap in
|
||||
ocanren {
|
||||
{ v_w == ZeroWV & w' == NeverWr } |
|
||||
{ v_w == SmthWV & w' == MayWr } |
|
||||
{ v_w == OneWV & w' == AlwaysWr }
|
||||
}
|
||||
|
||||
let rec tags_checko mem v tp =
|
||||
let open ReadVal in
|
||||
let open ReadCap in
|
||||
let open Type in
|
||||
let open Value in
|
||||
ocanren {
|
||||
{ fresh v_m, v_r, v_w,
|
||||
r, w in
|
||||
v == UnitV (v_m, v_r, v_w) &
|
||||
tp == UnitT (r, w) &
|
||||
{
|
||||
{ r == Rd & v_r == OneRV } |
|
||||
{ r == NRd & v_r == ZeroRV } |
|
||||
{ r == NRd & v_r == TopRV }
|
||||
} &
|
||||
writeval_to_capo v_w w
|
||||
} |
|
||||
{ fresh _stmts, _ts in
|
||||
v == FunV _stmts &
|
||||
tp == FunT _ts } |
|
||||
{ fresh id, _c, tp', v' in
|
||||
v == RefV id &
|
||||
tp == RefT (_c, tp') &
|
||||
mem_geto mem id v' &
|
||||
tags_checko mem v' tp' } |
|
||||
{ fresh vs, tps in
|
||||
v == TupleV vs &
|
||||
tp == TupleT tps &
|
||||
List.mapo (tags_checko mem) vs tps }
|
||||
}
|
||||
|
||||
(* - statement evaluation *)
|
||||
(* TODO *)
|
||||
|
||||
let rec stmt_addarg_foldero vals st_with_id mtp e st_with_id' = ocanren {
|
||||
fresh st, x, m, tp, st' in
|
||||
|
|
@ -920,16 +1149,28 @@ struct
|
|||
addargo st vals x tp e st' &
|
||||
st_with_id' == Std.pair st' (Nat.s x)
|
||||
}
|
||||
and stmt_eval_func_foldero mem types vals visited stmt visited' =
|
||||
and f_tags_check_foldero mem vals x mtp x' = ocanren {
|
||||
fresh m, tp, id', v' in
|
||||
mtp == Std.pair m tp &
|
||||
vals_assoco x vals id' &
|
||||
mem_geto mem id' v' &
|
||||
tags_checko mem v' tp &
|
||||
x' == Nat.s x
|
||||
}
|
||||
and stmt_eval_func_foldero mem types vals tps visited stmt visited' =
|
||||
let open StEnv in
|
||||
ocanren {
|
||||
{ fresh visited_add, st,
|
||||
st', mem', types', vals' in
|
||||
st', mem', types', vals',
|
||||
_x', visited'' in
|
||||
not_visited_checko visited stmt &
|
||||
visited_addo visited stmt visited_add &
|
||||
st == StEnv (mem, types, vals, visited_add) &
|
||||
stmt_evalo st stmt st' &
|
||||
st' == StEnv (mem', types', vals', visited') } |
|
||||
st' == StEnv (mem', types', vals', visited'') &
|
||||
list_foldlo (f_tags_check_foldero mem' vals') 0 tps _x' &
|
||||
visited' == visited''
|
||||
} |
|
||||
{ visited_checko visited stmt &
|
||||
visited == visited' }
|
||||
}
|
||||
|
|
@ -939,7 +1180,7 @@ struct
|
|||
fresh m, tp, st in
|
||||
Std.pair m tp == mtp &
|
||||
st == StEnv (mem, types, vals, visited) &
|
||||
argspoileo st m tp e mem'
|
||||
argsspoileo st m tp e mem'
|
||||
}
|
||||
and stmt_evalo st s st' =
|
||||
let open StEnv in
|
||||
|
|
@ -950,6 +1191,7 @@ struct
|
|||
let open TypesEnv in
|
||||
let open ValsEnv in
|
||||
let open RevPath in
|
||||
let open Action in
|
||||
ocanren {
|
||||
fresh mem, types, vals, visited in
|
||||
st == StEnv (mem, types, vals, visited) &
|
||||
|
|
@ -979,7 +1221,7 @@ struct
|
|||
(Std.pair st_call 0) tps es
|
||||
(Std.pair state_with_args _arg_id) &
|
||||
state_with_args == StEnv (mem_swa, types_swa, vals_swa, visited_swa) &
|
||||
list_foldlo (stmt_eval_func_foldero mem_swa types_swa vals_swa) visited_swa fstmts visited' &
|
||||
list_foldlo (stmt_eval_func_foldero mem_swa types_swa vals_swa tps) visited_swa fstmts visited' &
|
||||
(* TODO: FIXME check left or right order *)
|
||||
list_foldl2o (stmt_eval_spoil_foldero types vals (* NOTE: not important*) visited')
|
||||
mem tps es mem_spoiled &
|
||||
|
|
@ -995,13 +1237,25 @@ struct
|
|||
vals_assoco x vals id &
|
||||
mem_geto mem id v &
|
||||
pathrevo p VarRP rp &
|
||||
valupdo mem v rp ZeroV (Std.pair mem_upd v_upd) &
|
||||
valupdo mem v rp AlwaysWriteA (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
|
||||
{ fresh p, tp, _r, _w, x, id, v, rp,
|
||||
mem_upd, v_upd, mem_set in
|
||||
s == ReadS p &
|
||||
pathvalo mem vals p ZeroV &
|
||||
st == st' } |
|
||||
pathtypeo types p tp &
|
||||
tp == UnitT (_r, _w) &
|
||||
pathvaro p x &
|
||||
vals_assoco x vals id &
|
||||
mem_geto mem id v &
|
||||
pathrevo p VarRP rp &
|
||||
valupdo mem v rp ReadA (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 *)
|
||||
(* s == ReadS p & *)
|
||||
(* pathvalo mem vals p ZeroV & *)
|
||||
(* st == st' } | *)
|
||||
{ fresh sl, sr, stl in
|
||||
s == SeqS (sl, sr) &
|
||||
stmt_evalo st sl stl &
|
||||
|
|
|
|||
File diff suppressed because one or more lines are too long
|
|
@ -16,6 +16,7 @@ open WriteCap
|
|||
open InCap
|
||||
open OutCap
|
||||
open Mode
|
||||
open StEnv
|
||||
|
||||
@type answer =
|
||||
StEnv.ground GT.list with show
|
||||
|
|
@ -26,19 +27,31 @@ open Mode
|
|||
|
||||
(* - shortcuts *)
|
||||
|
||||
(* TODO *)
|
||||
|
||||
(* NOTE: redo with fold ?? *)
|
||||
let rec seqo stmts stmt' = ocanren {
|
||||
{ stmts == [] & stmt' == SkipS } |
|
||||
{ fresh s in
|
||||
stmts == [s] &
|
||||
stmt' == s } |
|
||||
{ fresh s, s', ss, stmt_rest' in
|
||||
stmts == s :: s' :: ss &
|
||||
seqo (s' :: ss) stmt_rest' &
|
||||
stmt' == SeqS(s, stmt_rest')
|
||||
let seq_foldero stmt_acc stmt stmt_acc' = ocanren {
|
||||
stmt_acc' == SeqS(stmt, stmt_acc)
|
||||
}
|
||||
let seqo stmts stmt' = ocanren {
|
||||
list_foldro seq_foldero SkipS stmts stmt'
|
||||
}
|
||||
(* ocanren { *)
|
||||
(* { stmts == [] & stmt' == SkipS } | *)
|
||||
(* { fresh s in *)
|
||||
(* stmts == [s] & *)
|
||||
(* stmt' == s } | *)
|
||||
(* { fresh s, s', ss, stmt_rest' in *)
|
||||
(* stmts == s :: s' :: ss & *)
|
||||
(* seqo (s' :: ss) stmt_rest' & *)
|
||||
(* stmt' == SeqS(s, stmt_rest') *)
|
||||
(* } *)
|
||||
(* } *)
|
||||
|
||||
let deref_accesso id v p' = ocanren {
|
||||
p' == DerefP (AccessP (VarP v, id))
|
||||
}
|
||||
|
||||
let access_deref_accesso id_ext id_int v p' = ocanren {
|
||||
p' == AccessP (DerefP (AccessP (VarP v, id_int)), id_ext)
|
||||
}
|
||||
|
||||
(* - basic var tests *)
|
||||
|
|
@ -120,6 +133,18 @@ let prog_eval_t_simple_var_wr_rd _ = show(answer) (Stream.take (run q
|
|||
|
||||
(* - basic call tests *)
|
||||
|
||||
(* NOTE: should add ? *)
|
||||
(* let prog_eval_t_simple_call_noarg _ = show(answer) (Stream.take (run q *)
|
||||
(* (fun q -> ocanren { *)
|
||||
(* fresh prog, xg, fg, xd, fd in *)
|
||||
(* globals_min_ido xg & *)
|
||||
(* fg == Nat.s xg & *)
|
||||
(* xd == VarD (UnitT (Rd, NeverWr), UnitE) & *)
|
||||
(* fd == FunD ([], SkipS) & *)
|
||||
(* prog == Prg ([xd; fd], CallS (VarP fg, [])) & *)
|
||||
(* prog_evalo prog q }) *)
|
||||
(* (fun q -> q#reify (StEnv.prj_exn)))) *)
|
||||
|
||||
let prog_eval_t_simple_call_rd _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xg, fg, xd, fd in
|
||||
|
|
@ -137,9 +162,9 @@ let prog_eval_t_simple_call_rd_ref _ = show(answer) (Stream.take (run q
|
|||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
xd == VarD (UnitT (Rd, MayWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))],
|
||||
xd == VarD (UnitT (Rd, NeverWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, NeverWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))],
|
||||
ReadS (DerefP (VarP 0))) &
|
||||
prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
|
||||
prog_evalo prog q })
|
||||
|
|
@ -151,9 +176,9 @@ let prog_eval_t_simple_call_wr _ = show(answer) (Stream.take (run q
|
|||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
xd == VarD (UnitT (Rd, MayWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))],
|
||||
xd == VarD (UnitT (NRd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
|
||||
WriteS (DerefP (VarP 0))) &
|
||||
prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
|
||||
prog_evalo prog q })
|
||||
|
|
@ -194,9 +219,9 @@ let prog_eval_t_simple_call_ref_wr _ = show(answer) (Stream.take (run q
|
|||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
|
||||
xd == VarD (UnitT (NRd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
|
||||
WriteS (DerefP (VarP 0))) &
|
||||
prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
|
||||
prog_evalo prog q })
|
||||
|
|
@ -223,9 +248,9 @@ let prog_eval_t_simple_call_ref_wr_with_fix _ = show(answer) (Stream.take (run q
|
|||
globals_min_ido xg &
|
||||
yg == Nat.s xg &
|
||||
fg == Nat.s yg &
|
||||
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
|
||||
xd == VarD (UnitT (NRd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
|
||||
WriteS (DerefP (VarP 0))) &
|
||||
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
|
||||
SeqS (WriteS (DerefP (VarP yg)),
|
||||
|
|
@ -242,9 +267,9 @@ let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q
|
|||
f2g == Nat.s fg &
|
||||
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
|
||||
WriteS (DerefP (VarP 0))) &
|
||||
f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))],
|
||||
f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
|
||||
SeqS (CallS (VarP fg, [PathE (VarP 0)]),
|
||||
WriteS (DerefP (VarP 0)))) &
|
||||
prog == Prg ([xd; yd; fd; f2d], SeqS (CallS (VarP f2g, [PathE (VarP yg)]),
|
||||
|
|
@ -260,7 +285,7 @@ let prog_eval_t_call_in_call_rec _ = show(answer) (Stream.take (run q
|
|||
fg == Nat.s yg &
|
||||
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))],
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
|
||||
SeqS (CallS (VarP fg, [PathE (VarP 0)]),
|
||||
WriteS (DerefP (VarP 0)))) &
|
||||
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
|
||||
|
|
@ -295,7 +320,7 @@ let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q
|
|||
fg == Nat.s yg &
|
||||
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))],
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))],
|
||||
SeqS (WriteS (VarP xg),
|
||||
ReadS (DerefP (VarP 0)))) &
|
||||
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
|
||||
|
|
@ -363,10 +388,10 @@ let prog_eval_t_call_with_dif_mods_cp _ = show(answer) (Stream.take (run q
|
|||
WriteS (DerefP (VarP 1));
|
||||
WriteS (DerefP (VarP 2));
|
||||
WriteS (DerefP (VarP 3))] fstmts &
|
||||
fd == FunD ([(Mode (NIn, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)));
|
||||
fd == FunD ([(Mode (NIn, NOut), RefT (Cp, UnitT (NRd, NeverWr)));
|
||||
(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)));
|
||||
(Mode (NIn, Out), RefT (Cp, UnitT (NRd, AlwaysWr)));
|
||||
(Mode (In, Out), RefT (Cp, UnitT (Rd, AlwaysWr)))],
|
||||
(Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr)));
|
||||
(Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))],
|
||||
fstmts) &
|
||||
seqo [CallS (VarP fg, [PathE (VarP yg);
|
||||
PathE (VarP y2g);
|
||||
|
|
@ -454,7 +479,7 @@ let prog_cp_cap_synt_t_simple_call_ref_wr _ = show(answerCpCap) (Stream.take (ru
|
|||
fg == Nat.s yg &
|
||||
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (Rd, AlwaysWr)))],
|
||||
fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (NRd, AlwaysWr)))],
|
||||
WriteS (DerefP (VarP 0))) &
|
||||
prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
|
||||
prog_evalo prog st })
|
||||
|
|
@ -483,7 +508,7 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr _ = show(answerCpCap) (Stream.take
|
|||
fg == Nat.s yg &
|
||||
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (Rd, AlwaysWr)))],
|
||||
fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (NRd, AlwaysWr)))],
|
||||
WriteS (DerefP (VarP 0))) &
|
||||
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
|
||||
ReadS (DerefP (VarP yg)))) &
|
||||
|
|
@ -506,7 +531,158 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.tak
|
|||
prog_evalo prog st })
|
||||
(fun q -> q#reify (CopyCap.prj_exn))))
|
||||
|
||||
(* - complex tests *)
|
||||
(* - presentation tests *)
|
||||
|
||||
(* simple types *)
|
||||
|
||||
let prog_eval_t_presentation_simple_tp _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xbg, xg,
|
||||
ybg, yg,
|
||||
zbg, zg,
|
||||
kbg, kg,
|
||||
fg, wg, gg, rg,
|
||||
xbd, xd,
|
||||
ybd, yd,
|
||||
zbd, zd,
|
||||
kbd, kd,
|
||||
fd, wd, gd, rd,
|
||||
fstmts, gstmts,
|
||||
stmts in
|
||||
globals_min_ido xbg &
|
||||
xg == Nat.s xbg &
|
||||
ybg == Nat.s xg &
|
||||
yg == Nat.s ybg &
|
||||
zbg == Nat.s yg &
|
||||
zg == Nat.s zbg &
|
||||
kbg == Nat.s zg &
|
||||
kg == Nat.s kbg &
|
||||
fg == Nat.s kg &
|
||||
wg == Nat.s fg &
|
||||
gg == Nat.s wg &
|
||||
rg == Nat.s gg &
|
||||
xbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xbg) &
|
||||
ybd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE ybg) &
|
||||
zbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE zbg) &
|
||||
kbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE kbg) &
|
||||
seqo [ReadS (DerefP (VarP 0));
|
||||
WriteS (DerefP (VarP 0));
|
||||
ReadS (DerefP (VarP 1))] fstmts &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)));
|
||||
(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))],
|
||||
fstmts) &
|
||||
wd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, MayWr)))],
|
||||
ChoiceS (WriteS (DerefP (VarP 0)), SkipS)) &
|
||||
seqo [WriteS (DerefP (VarP 0));
|
||||
ChoiceS (WriteS (DerefP (VarP 1)), WriteS (DerefP (VarP 0)));
|
||||
ReadS (DerefP (VarP 0));
|
||||
ReadS (DerefP (VarP 1))] gstmts &
|
||||
gd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)));
|
||||
(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))],
|
||||
gstmts) &
|
||||
rd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))],
|
||||
ReadS (DerefP (VarP 0))) &
|
||||
seqo [
|
||||
CallS (VarP wg, [PathE (VarP xg)]);
|
||||
CallS (VarP rg, [PathE (VarP xg)]);
|
||||
CallS (VarP fg, [PathE (VarP xg); PathE (VarP yg)]);
|
||||
CallS (VarP rg, [PathE (VarP yg)]);
|
||||
CallS (VarP gg, [PathE (VarP zg); PathE (VarP kg)]);
|
||||
CallS (VarP wg, [PathE (VarP zg)]);
|
||||
WriteS (DerefP (VarP zg));
|
||||
CallS (VarP fg, [PathE (VarP yg); PathE (VarP zg)]);
|
||||
CallS (VarP rg, [PathE (VarP kg)])
|
||||
] stmts &
|
||||
prog == Prg ([xbd; xd;
|
||||
ybd; yd;
|
||||
zbd; zd;
|
||||
kbd; kd;
|
||||
fd; wd; gd; rd],
|
||||
stmts) &
|
||||
prog_evalo prog q
|
||||
})
|
||||
(fun q -> q#reify (StEnv.prj_exn))))
|
||||
|
||||
let prog_synt_t_presentation_simple_tp _ = show(answerCpCapList) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog, xbg, xg,
|
||||
ybg, yg,
|
||||
zbg, zg,
|
||||
kbg, kg,
|
||||
fg, wg, gg, rg,
|
||||
xbd, xd,
|
||||
ybd, yd,
|
||||
zbd, zd,
|
||||
kbd, kd,
|
||||
fd, wd, gd, rd,
|
||||
fstmts, gstmts,
|
||||
stmts,
|
||||
c_fx, c_fy, c_wx, c_gx, c_gy, c_rx,
|
||||
st in
|
||||
globals_min_ido xbg &
|
||||
xg == Nat.s xbg &
|
||||
ybg == Nat.s xg &
|
||||
yg == Nat.s ybg &
|
||||
zbg == Nat.s yg &
|
||||
zg == Nat.s zbg &
|
||||
kbg == Nat.s zg &
|
||||
kg == Nat.s kbg &
|
||||
fg == Nat.s kg &
|
||||
wg == Nat.s fg &
|
||||
gg == Nat.s wg &
|
||||
rg == Nat.s gg &
|
||||
xbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xbg) &
|
||||
ybd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE ybg) &
|
||||
zbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE zbg) &
|
||||
kbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
|
||||
kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE kbg) &
|
||||
seqo [ReadS (DerefP (VarP 0));
|
||||
WriteS (DerefP (VarP 0));
|
||||
ReadS (DerefP (VarP 1))] fstmts &
|
||||
fd == FunD ([(Mode (In, NOut), RefT (c_fx, UnitT (Rd, AlwaysWr)));
|
||||
(Mode (In, NOut), RefT (c_fy, UnitT (Rd, NeverWr)))],
|
||||
fstmts) &
|
||||
wd == FunD ([(Mode (In, NOut), RefT (c_wx, UnitT (NRd, MayWr)))],
|
||||
ChoiceS (WriteS (DerefP (VarP 0)), SkipS)) &
|
||||
seqo [WriteS (DerefP (VarP 0));
|
||||
ChoiceS (WriteS (DerefP (VarP 1)), WriteS (DerefP (VarP 0)));
|
||||
ReadS (DerefP (VarP 0));
|
||||
ReadS (DerefP (VarP 1))] gstmts &
|
||||
gd == FunD ([(Mode (In, NOut), RefT (c_gx, UnitT (NRd, AlwaysWr)));
|
||||
(Mode (In, NOut), RefT (c_gy, UnitT (Rd, MayWr)))],
|
||||
gstmts) &
|
||||
rd == FunD ([(Mode (In, NOut), RefT (c_rx, UnitT (Rd, NeverWr)))],
|
||||
ReadS (DerefP (VarP 0))) &
|
||||
seqo [
|
||||
CallS (VarP wg, [PathE (VarP xg)]);
|
||||
CallS (VarP rg, [PathE (VarP xg)]);
|
||||
CallS (VarP fg, [PathE (VarP xg); PathE (VarP yg)]);
|
||||
CallS (VarP rg, [PathE (VarP yg)]);
|
||||
CallS (VarP gg, [PathE (VarP zg); PathE (VarP kg)]);
|
||||
CallS (VarP wg, [PathE (VarP zg)]);
|
||||
WriteS (DerefP (VarP zg));
|
||||
CallS (VarP fg, [PathE (VarP yg); PathE (VarP zg)]);
|
||||
CallS (VarP rg, [PathE (VarP kg)])
|
||||
] stmts &
|
||||
prog == Prg ([xbd; xd;
|
||||
ybd; yd;
|
||||
zbd; zd;
|
||||
kbd; kd;
|
||||
fd; wd; gd; rd],
|
||||
stmts) &
|
||||
prog_evalo prog st &
|
||||
q == [c_fx; c_fy; c_wx; c_gx; c_gy; c_rx]
|
||||
})
|
||||
(fun q -> q#reify (List.prj_exn CopyCap.prj_exn))))
|
||||
|
||||
(* complex type *)
|
||||
|
||||
let deref_accesso id v p' = ocanren {
|
||||
p' == DerefP (AccessP (VarP v, id))
|
||||
|
|
@ -516,6 +692,256 @@ let access_deref_accesso id_ext id_int v p' = ocanren {
|
|||
p' == AccessP (DerefP (AccessP (VarP v, id_int)), id_ext)
|
||||
}
|
||||
|
||||
(* --- *)
|
||||
|
||||
let p_rw_unitTo tp = ocanren {
|
||||
(* fresh r, w in *)
|
||||
tp == UnitT (Rd, AlwaysWr)
|
||||
}
|
||||
|
||||
let p_rw_userTo tp = ocanren {
|
||||
fresh x, y, z in
|
||||
p_rw_unitTo x &
|
||||
p_rw_unitTo y &
|
||||
p_rw_unitTo z &
|
||||
tp == TupleT [x; y; z]
|
||||
}
|
||||
|
||||
let p_rw_dataTo tp = ocanren {
|
||||
fresh x, y in
|
||||
p_rw_unitTo x &
|
||||
p_rw_unitTo y &
|
||||
tp == TupleT [x; y]
|
||||
}
|
||||
|
||||
let p_rw_timeTo tp = ocanren {
|
||||
p_rw_unitTo tp
|
||||
}
|
||||
|
||||
let p_rw_requestTo cu cd ct tp = ocanren {
|
||||
fresh userT, dataT, timeT in
|
||||
p_rw_userTo userT &
|
||||
p_rw_dataTo dataT &
|
||||
p_rw_timeTo timeT &
|
||||
tp == TupleT [RefT (cu, userT);
|
||||
RefT (cd, dataT);
|
||||
RefT (ct, timeT)]
|
||||
}
|
||||
|
||||
(* --- *)
|
||||
|
||||
let p_any_unitTo tp = ocanren {
|
||||
fresh r, w in
|
||||
tp == UnitT (r, w)
|
||||
}
|
||||
|
||||
let p_any_userTo tp = ocanren {
|
||||
fresh x, y, z in
|
||||
p_any_unitTo x &
|
||||
p_any_unitTo y &
|
||||
p_any_unitTo z &
|
||||
tp == TupleT [x; y; z]
|
||||
}
|
||||
|
||||
let p_any_dataTo tp = ocanren {
|
||||
fresh x, y in
|
||||
p_any_unitTo x &
|
||||
p_any_unitTo y &
|
||||
tp == TupleT [x; y]
|
||||
}
|
||||
|
||||
let p_any_timeTo tp = ocanren {
|
||||
p_any_unitTo tp
|
||||
}
|
||||
|
||||
let p_any_requestTo cu cd ct tp = ocanren {
|
||||
fresh userT, dataT, timeT in
|
||||
p_any_userTo userT &
|
||||
p_any_dataTo dataT &
|
||||
p_any_timeTo timeT &
|
||||
tp == TupleT [RefT (cu, userT);
|
||||
RefT (cd, dataT);
|
||||
RefT (ct, timeT)]
|
||||
}
|
||||
|
||||
(* --- *)
|
||||
|
||||
let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog,
|
||||
userT, dataT, timeT, requestT,
|
||||
requestArgsT,
|
||||
userE, dataE, timeE, requestE,
|
||||
userVID, dataVID, timeVID, requestVID,
|
||||
sendFID, sendD, sendBranchStmts, sendStmts,
|
||||
stmts in
|
||||
globals_min_ido userVID &
|
||||
dataVID == Nat.s userVID &
|
||||
timeVID == Nat.s dataVID &
|
||||
requestVID == Nat.s timeVID &
|
||||
sendFID == Nat.s requestVID &
|
||||
|
||||
p_rw_userTo userT &
|
||||
p_rw_dataTo dataT &
|
||||
p_rw_timeTo timeT &
|
||||
p_rw_requestTo Cp Cp Cp requestT &
|
||||
p_any_requestTo Cp Cp Cp requestArgsT & (* NOTE: for now *)
|
||||
|
||||
userE == TupleE [UnitE; UnitE; UnitE] &
|
||||
dataE == TupleE [UnitE; UnitE] &
|
||||
timeE == UnitE &
|
||||
requestE == TupleE [RefE userVID; RefE dataVID; RefE timeVID] &
|
||||
|
||||
fresh data_p0, data_p1, time_p,
|
||||
user_id_p, user_name_p, user_surname_p in
|
||||
access_deref_accesso 0 1 0 data_p0 &
|
||||
access_deref_accesso 1 1 0 data_p1 &
|
||||
deref_accesso 2 0 time_p &
|
||||
access_deref_accesso 0 0 0 user_id_p &
|
||||
access_deref_accesso 1 0 0 user_name_p &
|
||||
access_deref_accesso 2 0 0 user_surname_p &
|
||||
seqo [ReadS data_p0;
|
||||
ReadS data_p1;
|
||||
WriteS data_p0;
|
||||
WriteS data_p1;
|
||||
|
||||
ReadS user_name_p;
|
||||
WriteS user_name_p] sendBranchStmts &
|
||||
seqo [sendBranchStmts; (* TMP *)
|
||||
(* TODO: FIXME *)
|
||||
(* ChoiceS (sendBranchStmts, SkipS); *)
|
||||
WriteS time_p;
|
||||
|
||||
ReadS data_p0;
|
||||
ReadS data_p1;
|
||||
ReadS time_p;
|
||||
ReadS user_id_p;
|
||||
ReadS user_name_p;
|
||||
ReadS user_surname_p] sendStmts &
|
||||
(* sendStmts == SkipS & *)
|
||||
sendD == FunD ([(Mode (In, NOut), requestArgsT)], sendStmts) &
|
||||
|
||||
fresh time_gp, user_name_gp, user_surname_gp in
|
||||
deref_accesso 2 requestVID time_gp &
|
||||
access_deref_accesso 1 0 requestVID user_name_gp &
|
||||
access_deref_accesso 2 0 requestVID user_surname_gp &
|
||||
seqo [
|
||||
CallS (VarP sendFID, [PathE (VarP requestVID)]);
|
||||
WriteS time_gp;
|
||||
(* TODO: FIXME *)
|
||||
(* ChoiceS (ReadS user_name_gp, *)
|
||||
(* ReadS user_surname_gp); *)
|
||||
ReadS user_name_gp; (* TMP *)
|
||||
ReadS user_surname_gp; (* TMP *)
|
||||
ReadS time_gp
|
||||
] stmts &
|
||||
prog == Prg ([
|
||||
VarD (userT, userE);
|
||||
VarD (dataT, dataE);
|
||||
VarD (timeT, timeE);
|
||||
VarD (requestT, requestE);
|
||||
sendD
|
||||
],
|
||||
stmts
|
||||
) &
|
||||
prog_evalo prog q
|
||||
})
|
||||
(fun q -> q#reify (StEnv.prj_exn))))
|
||||
|
||||
let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take (run q
|
||||
(fun q -> ocanren {
|
||||
fresh prog,
|
||||
userT, dataT, timeT, requestT,
|
||||
requestArgsT,
|
||||
userE, dataE, timeE, requestE,
|
||||
userVID, dataVID, timeVID, requestVID,
|
||||
sendFID, sendD, sendBranchStmts, sendStmts,
|
||||
stmts,
|
||||
st, c_u, c_d, c_t in
|
||||
globals_min_ido userVID &
|
||||
dataVID == Nat.s userVID &
|
||||
timeVID == Nat.s dataVID &
|
||||
requestVID == Nat.s timeVID &
|
||||
sendFID == Nat.s requestVID &
|
||||
|
||||
p_rw_userTo userT &
|
||||
p_rw_dataTo dataT &
|
||||
p_rw_timeTo timeT &
|
||||
p_rw_requestTo Cp Cp Cp requestT &
|
||||
p_any_requestTo c_u c_d c_t requestArgsT & (* NOTE: for now *)
|
||||
|
||||
userE == TupleE [UnitE; UnitE; UnitE] &
|
||||
dataE == TupleE [UnitE; UnitE] &
|
||||
timeE == UnitE &
|
||||
requestE == TupleE [RefE userVID; RefE dataVID; RefE timeVID] &
|
||||
|
||||
fresh data_p0, data_p1, time_p,
|
||||
user_id_p, user_name_p, user_surname_p in
|
||||
access_deref_accesso 0 1 0 data_p0 &
|
||||
access_deref_accesso 1 1 0 data_p1 &
|
||||
deref_accesso 2 0 time_p &
|
||||
access_deref_accesso 0 0 0 user_id_p &
|
||||
access_deref_accesso 1 0 0 user_name_p &
|
||||
access_deref_accesso 2 0 0 user_surname_p &
|
||||
seqo [ReadS data_p0;
|
||||
ReadS data_p1;
|
||||
WriteS data_p0;
|
||||
WriteS data_p1;
|
||||
|
||||
ReadS user_name_p;
|
||||
WriteS user_name_p] sendBranchStmts &
|
||||
seqo [sendBranchStmts; (* TMP *)
|
||||
(* TODO: FIXME *)
|
||||
(* ChoiceS (sendBranchStmts, SkipS); *)
|
||||
WriteS time_p;
|
||||
|
||||
ReadS data_p0;
|
||||
ReadS data_p1;
|
||||
ReadS time_p;
|
||||
ReadS user_id_p;
|
||||
ReadS user_name_p;
|
||||
ReadS user_surname_p] sendStmts &
|
||||
(* sendStmts == SkipS & *)
|
||||
sendD == FunD ([(Mode (In, NOut), requestArgsT)], sendStmts) &
|
||||
|
||||
fresh time_gp, user_name_gp, user_surname_gp in
|
||||
deref_accesso 2 requestVID time_gp &
|
||||
access_deref_accesso 1 0 requestVID user_name_gp &
|
||||
access_deref_accesso 2 0 requestVID user_surname_gp &
|
||||
seqo [
|
||||
CallS (VarP sendFID, [PathE (VarP requestVID)]);
|
||||
WriteS time_gp;
|
||||
(* TODO: FIXME *)
|
||||
(* ChoiceS (ReadS user_name_gp, *)
|
||||
(* ReadS user_surname_gp); *)
|
||||
ReadS user_name_gp; (* TMP *)
|
||||
ReadS user_surname_gp; (* TMP *)
|
||||
ReadS time_gp
|
||||
] stmts &
|
||||
prog == Prg ([
|
||||
VarD (userT, userE);
|
||||
VarD (dataT, dataE);
|
||||
VarD (timeT, timeE);
|
||||
VarD (requestT, requestE);
|
||||
sendD
|
||||
],
|
||||
stmts
|
||||
) &
|
||||
prog_evalo prog st &
|
||||
q == [c_u; c_d; c_t]
|
||||
})
|
||||
(fun q -> q#reify (List.prj_exn CopyCap.prj_exn))))
|
||||
|
||||
(* - complex tests *)
|
||||
|
||||
(* let deref_accesso id v p' = ocanren { *)
|
||||
(* p' == DerefP (AccessP (VarP v, id)) *)
|
||||
(* } *)
|
||||
|
||||
(* let access_deref_accesso id_ext id_int v p' = ocanren { *)
|
||||
(* p' == AccessP (DerefP (AccessP (VarP v, id_int)), id_ext) *)
|
||||
(* } *)
|
||||
|
||||
let access_deref_access_deref_accesso id_ext id_mid id_int v p' = ocanren {
|
||||
p' == AccessP (DerefP (AccessP (DerefP (AccessP (VarP v, id_int)), id_mid)), id_ext)
|
||||
}
|
||||
|
|
@ -655,11 +1081,84 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q
|
|||
prog_evalo prog q })
|
||||
(fun q -> q#reify (StEnv.prj_exn))))
|
||||
|
||||
(* rw versions *)
|
||||
|
||||
let rw_unitTo tp = ocanren {
|
||||
(* fresh r, w in *)
|
||||
tp == UnitT (Rd, AlwaysWr)
|
||||
}
|
||||
|
||||
let rw_user_utilsTo tp = ocanren {
|
||||
fresh x, y in
|
||||
rw_unitTo x &
|
||||
rw_unitTo y &
|
||||
tp == TupleT [x; y]
|
||||
}
|
||||
|
||||
let rw_user_infoTo tp = ocanren {
|
||||
fresh x, y, z in
|
||||
rw_unitTo x &
|
||||
rw_unitTo y &
|
||||
rw_unitTo z &
|
||||
tp == TupleT [x; y; z]
|
||||
}
|
||||
|
||||
let rw_versionTo tp = ocanren {
|
||||
fresh x, y, z in
|
||||
rw_unitTo x &
|
||||
rw_unitTo y &
|
||||
rw_unitTo z &
|
||||
tp == TupleT [x; y; z]
|
||||
}
|
||||
|
||||
let rw_utilsTo tp = ocanren {
|
||||
fresh x, y in
|
||||
rw_unitTo x &
|
||||
rw_unitTo y &
|
||||
tp == TupleT [x; y]
|
||||
}
|
||||
|
||||
let rw_dataTo tp = ocanren {
|
||||
rw_unitTo tp
|
||||
}
|
||||
|
||||
let rw_op_dateTo tp = ocanren {
|
||||
rw_unitTo tp
|
||||
}
|
||||
|
||||
let rw_userTo cu ci tp = ocanren {
|
||||
fresh utilsT, infoT in
|
||||
rw_user_infoTo infoT &
|
||||
rw_user_utilsTo utilsT &
|
||||
tp == TupleT [RefT (cu, utilsT) (* 0 utils *);
|
||||
RefT (ci, infoT) (* 1 info *)]
|
||||
}
|
||||
|
||||
let rw_requestTo cus cv cut cd cus_u cus_i tp = ocanren {
|
||||
fresh userT, versionT, utilsT, dataT, op_dateT in
|
||||
rw_userTo cus_u cus_i userT &
|
||||
rw_versionTo versionT &
|
||||
rw_utilsTo utilsT &
|
||||
rw_dataTo dataT &
|
||||
rw_op_dateTo op_dateT &
|
||||
tp == TupleT [RefT (cus, userT) (* 0 user *);
|
||||
RefT (cv, versionT) (* 1 version *);
|
||||
RefT (cut, utilsT) (* 2 utils *);
|
||||
RefT (cd, dataT) (* 3 data *);
|
||||
op_dateT (* 4 operation_date *)]
|
||||
}
|
||||
let rw_moded_requestTo cus cv cut cd cus_u cus_i tp = ocanren {
|
||||
fresh requestT in
|
||||
rw_requestTo cus cv cut cd cus_u cus_i requestT &
|
||||
tp == (Mode (In, NOut), requestT)
|
||||
}
|
||||
let rw_boxed_moded_requestTo tp = ocanren {
|
||||
fresh cus, cv, cut, cd, cus_u, cus_i in
|
||||
rw_moded_requestTo cus cv cut cd cus_u cus_i tp
|
||||
}
|
||||
|
||||
(* any versions *)
|
||||
|
||||
let any_unitTo tp = ocanren {
|
||||
fresh r, w in
|
||||
tp == UnitT (r, w)
|
||||
|
|
@ -667,40 +1166,40 @@ let any_unitTo tp = ocanren {
|
|||
|
||||
let any_user_utilsTo tp = ocanren {
|
||||
fresh x, y in
|
||||
rw_unitTo x &
|
||||
rw_unitTo y &
|
||||
any_unitTo x &
|
||||
any_unitTo y &
|
||||
tp == TupleT [x; y]
|
||||
}
|
||||
|
||||
let any_user_infoTo tp = ocanren {
|
||||
fresh x, y, z in
|
||||
rw_unitTo x &
|
||||
rw_unitTo y &
|
||||
rw_unitTo z &
|
||||
any_unitTo x &
|
||||
any_unitTo y &
|
||||
any_unitTo z &
|
||||
tp == TupleT [x; y; z]
|
||||
}
|
||||
|
||||
let any_versionTo tp = ocanren {
|
||||
fresh x, y, z in
|
||||
rw_unitTo x &
|
||||
rw_unitTo y &
|
||||
rw_unitTo z &
|
||||
any_unitTo x &
|
||||
any_unitTo y &
|
||||
any_unitTo z &
|
||||
tp == TupleT [x; y; z]
|
||||
}
|
||||
|
||||
let any_utilsTo tp = ocanren {
|
||||
fresh x, y in
|
||||
rw_unitTo x &
|
||||
rw_unitTo y &
|
||||
any_unitTo x &
|
||||
any_unitTo y &
|
||||
tp == TupleT [x; y]
|
||||
}
|
||||
|
||||
let any_dataTo tp = ocanren {
|
||||
rw_unitTo tp
|
||||
any_unitTo tp
|
||||
}
|
||||
|
||||
let any_op_dateTo tp = ocanren {
|
||||
rw_unitTo tp
|
||||
any_unitTo tp
|
||||
}
|
||||
|
||||
let any_userTo cu ci tp = ocanren {
|
||||
|
|
@ -767,13 +1266,13 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
|
|||
(* synt *)
|
||||
st in
|
||||
(* types *)
|
||||
any_unitTo uT_r_aw &
|
||||
any_user_utilsTo user_utilsT &
|
||||
any_user_infoTo user_infoT &
|
||||
any_userTo Cp Cp userT &
|
||||
any_versionTo versionT &
|
||||
any_utilsTo utilsT &
|
||||
any_requestTo Cp Cp Cp Cp Cp Cp requestT &
|
||||
rw_unitTo uT_r_aw &
|
||||
rw_user_utilsTo user_utilsT &
|
||||
rw_user_infoTo user_infoT &
|
||||
rw_userTo Cp Cp userT &
|
||||
rw_versionTo versionT &
|
||||
rw_utilsTo utilsT &
|
||||
rw_requestTo Cp Cp Cp Cp Cp Cp requestT &
|
||||
(* moded_requestTo moded_requestT & *)
|
||||
(* global vars init exprs *)
|
||||
user_utilsE == TupleE [UnitE (* 0 id *); UnitE] &
|
||||
|
|
@ -849,15 +1348,16 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
|
|||
send_allF &
|
||||
|
||||
fresh mrT_gvi, mrT_uv, mrT_s, mrT_sa in
|
||||
fresh gvi_c0, gvi_c1, gvi_c2, gvi_c3, gvi_c4, gvi_c5, mrT' in
|
||||
any_moded_requestTo gvi_c0 gvi_c1 gvi_c2 gvi_c3 gvi_c4 gvi_c5 mrT' &
|
||||
(* fresh gvi_c0, gvi_c1, gvi_c2, gvi_c3, gvi_c4, gvi_c5, mrT' in *)
|
||||
(* any_moded_requestTo gvi_c0 gvi_c1 gvi_c2 gvi_c3 gvi_c4 gvi_c5 mrT' & *)
|
||||
(* TODO *)
|
||||
(* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_gvi & *)
|
||||
(* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_uv & *)
|
||||
(* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_s & *)
|
||||
(* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_sa & *)
|
||||
any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_gvi &
|
||||
any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_uv &
|
||||
any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_s &
|
||||
any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_sa &
|
||||
|
||||
q == [gvi_c0; gvi_c1; gvi_c2; gvi_c3; gvi_c4; gvi_c5] &
|
||||
q == [Cp] &
|
||||
(* [gvi_c0; gvi_c1; gvi_c2; gvi_c3; gvi_c4; gvi_c5] & *)
|
||||
|
||||
prog == Prg ([
|
||||
VarD (user_utilsT, user_utilsE);
|
||||
|
|
@ -867,17 +1367,17 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
|
|||
VarD (utilsT, utilsE);
|
||||
VarD (uT_r_aw, UnitE); (* data *)
|
||||
VarD (requestT, requestE);
|
||||
FunD ([mrT'], get_version_idF);
|
||||
FunD ([mrT'], updated_versionF);
|
||||
FunD ([mrT'], sendF);
|
||||
FunD ([mrT'], send_allF)
|
||||
(* FunD ([mrT_gvi], get_version_idF); *)
|
||||
(* FunD ([mrT_uv], updated_versionF); *)
|
||||
(* FunD ([mrT_s], sendF); *)
|
||||
(* FunD ([mrT_sa], send_allF) *)
|
||||
(* FunD ([mrT'], get_version_idF); *)
|
||||
(* FunD ([mrT'], updated_versionF); *)
|
||||
(* FunD ([mrT'], sendF); *)
|
||||
(* FunD ([mrT'], send_allF) *)
|
||||
FunD ([mrT_gvi], get_version_idF);
|
||||
FunD ([mrT_uv], updated_versionF);
|
||||
FunD ([mrT_s], sendF);
|
||||
FunD ([mrT_sa], send_allF)
|
||||
],
|
||||
(* SkipS *)
|
||||
CallS (VarP send_allID, [PathE (VarP requestID)])
|
||||
) &
|
||||
prog_evalo prog st })
|
||||
(fun q -> q#reify (List.prj_exn CopyCap.prj_exn)))) (* TODO: list *)
|
||||
(fun q -> q#reify (List.prj_exn CopyCap.prj_exn))))
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue