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

Compare commits

base: st:a56a8ffebc958f4ecd7319b4938d952eb123d9d0
Branches Tags
st:main
st:lambdas_no_value
st:memory_ext
..
compare: st:18481550d3a1d2c82bbd257c158569211d414136
Branches Tags
st:main
st:lambdas_no_value
st:memory_ext

No commits in common. "a56a8ffebc958f4ecd7319b4938d952eb123d9d0" and "18481550d3a1d2c82bbd257c158569211d414136" have entirely different histories.
a56a8ffebc ... 18481550d3

3 changed files with 271 additions and 671 deletions
Download patch file Download diff file Expand all files Collapse all files

490
model_with_structures/analyzer.ml
View file

@ -59,26 +59,22 @@ struct
(* value model & memory model *) (* value model & memory model *)
(* type deepvalue = ZeroDV *) type deepvalue = ZeroDV
(* | SmthDV *) | SmthDV
(* | BotDV *) | BotDV
(* | FunDV of ((* data list * *) stmt) list *) | FunDV of ((* data list * *) stmt) list
(* | RefDV of deepvalue *) | RefDV of deepvalue
(* | TupleDV of deepvalue list *) | TupleDV of deepvalue list
type memval = ZeroMV | SmthMV | BotMV (* | TopMV ?? *) type value = ZeroV
type readval = ZeroRV | OneRV | TopRV | SmthV
type writeval = ZeroWV | SmthWV | OneWV | BotV
type value = UnitV of memval * readval * writeval
| FunV of ((* data list * *) stmt) list | FunV of ((* data list * *) stmt) list
| RefV of memid | RefV of memid
| TupleV of value list | TupleV of value list
type revpath = VarRP | DerefRP of revpath | AccessRP of revpath * data type revpath = VarRP | DerefRP of revpath | AccessRP of revpath * data
type action = ReadA | AlwaysWriteA | MayWriteA
(* TODO: any additional difference between rvalue and lvalue now ?? *) (* TODO: any additional difference between rvalue and lvalue now ?? *)
(* --- *) (* --- *)
@ -142,17 +138,16 @@ struct
let mem_set (mem : mem) (id : memid) (v : value) : mem = let mem_set (mem : mem) (id : memid) (v : value) : mem =
(list_replace (fst mem) (snd mem - id - 1) v, snd 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 *) let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with
(* | ZeroV -> ZeroDV *) | ZeroV -> ZeroDV
(* | SmthV -> SmthDV *) | SmthV -> SmthDV
(* | BotV -> BotDV *) | BotV -> BotDV
(* | FunV s -> FunDV s *) | FunV s -> FunDV s
(* | RefV id -> RefDV (v_to_deepv mem @@ mem_get mem id) *) | RefV id -> RefDV (v_to_deepv mem @@ mem_get mem id)
(* | TupleV vs -> TupleDV (List.map (v_to_deepv mem) vs) *) | TupleV vs -> TupleDV (List.map (v_to_deepv mem) vs)
let is_trivial_v (v : value) : bool = let is_trivial_v (v : value) : bool =
match v with | UnitV (_, _, _) -> true v == ZeroV || v == SmthV || v == BotV
| _ -> false
(* --- path accessors --- *) (* --- path accessors --- *)
@ -196,9 +191,19 @@ struct
(* - value construction *) (* - value construction *)
let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value =
match t, v with if is_trivial_v v
| UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV)) then match t with
| UnitT (NRd, _), UnitV _ -> (mem, UnitV (BotMV, ZeroRV, ZeroWV)) | 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) *)
| FunT _, FunV _ -> (mem, v) | FunT _, FunV _ -> (mem, v)
| RefT (Rf, _), RefV _ -> (mem, v) | RefT (Rf, _), RefV _ -> (mem, v)
| RefT (Cp, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in | RefT (Cp, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in
@ -210,75 +215,24 @@ struct
(mem', TupleV (List.rev vs')) (* TODO: FIXME: should reverse or not ?? *) (mem', TupleV (List.rev vs')) (* TODO: FIXME: should reverse or not ?? *)
| _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type" | _, _ -> 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 *) (* - value update *)
let rec valchange (mem : mem) (v : value) (p : revpath) (b : value) : mem * value = match p, v with let rec valupd (mem : mem) (v : value) (p : revpath) (b : value) : mem * value = match p, v with
| VarRP, _ -> (mem, b) | VarRP, _ -> (mem, b)
| DerefRP p, RefV id -> let (mem', v') = valchange mem (mem_get mem id) p b in | DerefRP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p b in
(mem_set mem' id v', RefV id) (mem_set mem' id v', RefV id)
| AccessRP (p, id), TupleV vs -> let (mem', v') = valchange mem (List.nth vs id) p b in | AccessRP (p, id), TupleV vs -> let (mem', v') = (* FIXME TMP Printf.printf "vs size=%i id=%i\n" (List.length vs) id; *)
(mem', TupleV (list_replace vs id v')) valupd mem (List.nth vs id) p b in
| _, _ -> raise @@ Typing_error "valupd" (* FIXME TMP Printf.printf "before return\n"; *)
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')) (mem', TupleV (list_replace vs id v'))
| _, _ -> raise @@ Typing_error "valupd" | _, _ -> raise @@ Typing_error "valupd"
(* - value combination *) (* - 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 = let rec valcomb (u : value) (v : value) : value =
match u, v with if is_trivial_v u && is_trivial_v v
| UnitV (u_m, u_r, u_w), UnitV (v_m, v_r, v_w) -> then (if u == v then u else BotV)
UnitV (memvalcomb u_m v_m, readvalcomb u_r v_r, writevalcomb u_w v_w) else match u, v with
| FunV ustmts, FunV vstmts -> FunV (ustmts @ vstmts) | FunV ustmts, FunV vstmts -> FunV (ustmts @ vstmts)
| RefV a, RefV b -> if a == b then u else raise @@ Typing_error "valcomb: ref" | 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) | TupleV us, TupleV vs -> TupleV (List.map2 valcomb us vs)
@ -292,7 +246,7 @@ struct
(* - expression evaluation *) (* - expression evaluation *)
let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with
| UnitE -> UnitV (ZeroMV, ZeroRV, ZeroWV) | UnitE -> ZeroV
| PathE p -> pathval mem vals p | PathE p -> pathval mem vals p
| RefE x -> RefV (vals_assoc x vals) | RefE x -> RefV (vals_assoc x vals)
| TupleE es -> TupleV (List.map (exprval mem vals) es) | TupleE es -> TupleV (List.map (exprval mem vals) es)
@ -333,64 +287,48 @@ struct
(* - call values spoil *) (* - call values spoil *)
(* TODO: check assignment type matches types separately later ?? *) (* TODO: check all cases *)
let is_correct_tags (r : read_cap) (w : write_cap) let is_correct_tags (v : value) (r : read_cap) (w : write_cap)
(m : mode) (c : copy_cap) : bool = (r' : read_cap) (w' : write_cap) (m : mode)
(snd m != Out || c == Rf) && (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) &&
(snd m != Out || w == AlwaysWr) && (snd m != Out || w == AlwaysWr) &&
(r != Rd || fst m == In) (* TODO: FIXME: check *)
((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr) &&
let tryread (r : read_cap) (v_m : memval) is_trivial_v v
(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) let rec valspoil (mem : mem) (v : value) (t : atype)
(m : mode) (c : copy_cap) (u : atype) (m : mode) (c : copy_cap)
: mem * value = match t, v with : mem * value = match t, u, v with
| UnitT (r, w), UnitV (v_m, v_r, v_w) -> | UnitT (r, w), UnitT (r', w'), _ ->
if not @@ is_correct_tags r w m c if not @@ is_trivial_v v
then raise @@ Typing_error "valspoil: trivial type tags combination is not correct" then raise @@ Typing_error "valspoil: unit, not trivial"
else else if not @@ is_correct_tags v r w r' w' m c
let v' = tryread r v_m v_r v_w in then raise @@ Typing_error "valspoil: unit, not correct"
if c == Cp || w == NeverWr else if snd m == NOut && c == Rf && (w == AlwaysWr || w == MayWr)
then (mem, v') then (mem, BotV)
else (match v' with else if snd m == Out && w == AlwaysWr
| UnitV (v_m', v_r', v_w') -> then (mem, ZeroV)
let (v_m'', v_r'', v_w'') = else (mem, v)
(if w == AlwaysWr | FunT ts, FunT us, FunV _ -> if ts == us then (mem, v) else raise @@ Typing_error "valspoil: fun"
then (memvmod AlwaysWriteA v_m', | RefT (ct, t), RefT (cu, u), RefV id ->
readvmod AlwaysWriteA v_r', let (mem', v') = valspoil mem (mem_get mem id) t u m ct in
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) (mem_set mem id v', RefV id)
| TupleT ts, TupleV vs -> | TupleT ts, TupleT us, TupleV vs ->
let folder = fun (mem, vs') t v -> let folder = fun (mem, vs') t u v ->
let (mem', v') = valspoil mem v t m c in (mem', v' :: vs') in let (mem', v') = valspoil mem v t u m c in (mem', v' :: vs') in
let (mem', vs') = List.fold_left2 folder (mem, []) ts vs in let (mem', vs') = list_foldl3 folder (mem, []) ts us vs in
(mem', TupleV (List.rev vs')) (mem', TupleV (List.rev vs'))
| _, _ -> raise @@ Typing_error "valspoil" | _, _, _ -> raise @@ Typing_error "valspoil"
(* full spoil *) (* full spoil *)
@ -399,11 +337,11 @@ struct
let x = pathvar p in let x = pathvar p in
let id = vals_assoc x vals in (* base var address *) let id = vals_assoc x vals in (* base var address *)
let b = pathval mem vals p in (* subvalue in var *) let b = pathval mem vals p in (* subvalue in var *)
(* let t' = pathtype types p in (* type of subvalue *) *) let t' = pathtype types p in (* type of subvalue *)
let (mem', b') = valspoil mem b t m Cp in (* spoil subvalue *) let (mem', b') = valspoil mem b t t' m Cp in (* spoil subvalue *)
(* TODO: FIXME: why copy (Cp)? maybe sometimes use top-level capability ? *) (* TODO: FIXME: why copy (Cp)? maybe sometimes use top-level capability ? *)
let pi = pathrev p VarRP in let pi = pathrev p VarRP in
let (mem'', v'') = valchange mem' (mem_get mem' id) pi b' in (* set subvalue into var *) let (mem'', v'') = valupd mem' (mem_get mem' id) pi b' in (* set subvalue into var *)
mem_set mem'' id v'' mem_set mem'' id v''
let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem = let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem =
@ -431,34 +369,15 @@ struct
(* NOTE: not needed due to performed optimization in stmt_eval *) (* 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 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 *) (* - statement evaluation *)
let rec stmt_eval (state : state) (s : stmt) : state = let rec stmt_eval (state : state) (s : stmt) : state =
match state with (mem, types, vals, visited) -> match s with match state with (mem, types, vals, visited) -> match s with
| SkipS -> state | SkipS -> state
| CallS (f, es) -> let v = pathval mem vals f in | CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *)
let t = pathtype types f in pathval mem vals f in
let t = (* FIXME TMP Printf.printf "call, before t\n"; *)
pathtype types f in
let types' : types = (fst types, fst types) in let types' : types = (fst types, fst types) in
let vals' : vals = (fst vals, fst vals) in let vals' : vals = (fst vals, fst vals) in
(match v, t with (match v, t with
@ -475,14 +394,7 @@ struct
if List.mem stmt visited_old if List.mem stmt visited_old
then stmt :: visited_old then stmt :: visited_old
else match stmt_eval (mem_swa, types_swa, vals_swa, stmt :: visited_old) stmt with else match stmt_eval (mem_swa, types_swa, vals_swa, stmt :: visited_old) stmt with
(mem_after_stmt, _, vals_after_stmt, visited_after_stmt) -> (_, _, _, visited_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 visited_swa
fstmts in fstmts in
let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *) let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *)
@ -500,28 +412,16 @@ struct
else let x = pathvar p in else let x = pathvar p in
let id = vals_assoc x vals in let id = vals_assoc x vals in
let pi = pathrev p VarRP in let pi = pathrev p VarRP in
let (mem', v') = valupd mem (mem_get mem id) pi AlwaysWriteA in let (mem', v') = valupd mem (mem_get mem id) pi ZeroV in
(mem_set mem' id v', types, vals, visited) (mem_set mem' id v', types, vals, visited)
| RefT _ -> raise @@ Eval_error "write: ref type" | RefT _ -> raise @@ Eval_error "write: ref type"
| TupleT _ -> raise @@ Eval_error "write: tuple type" | TupleT _ -> raise @@ Eval_error "write: tuple type"
| _ -> raise @@ Eval_error "write: type") | _ -> raise @@ Eval_error "write: type")
| ReadS p -> (match pathtype types p with | ReadS p -> if pathval mem vals p == SmthV || pathval mem vals p == BotV
| UnitT (_, _) -> then raise @@ Eval_error "read: spoiled value"
(* NOTE: not required *) else if pathval mem vals p != ZeroV
(* if r == NRd *) then raise @@ Eval_error "read: nontrivial value"
(* then raise @@ Eval_error "read: not read tag" *) else state
(* 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 | SeqS (sl, sr) -> let statel = stmt_eval state sl in
stmt_eval statel sr stmt_eval statel sr
| ChoiceS (sl, sr) -> let statel = stmt_eval state sl in | ChoiceS (sl, sr) -> let statel = stmt_eval state sl in
@ -618,30 +518,23 @@ struct
let rdS p = ReadS p let rdS p = ReadS p
let callS f args = CallS (f, args) let callS f args = CallS (f, args)
let uV m = UnitV (m, ZeroRV, ZeroWV)
(* - utils tests *) (* - 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%expect_test "mem add / get / set" =
let mem = empty_mem in let mem = empty_mem in
let (mem, id1) = mem_add mem @@ uV ZeroMV in let (mem, id1) = mem_add mem ZeroV in
let (mem, id2) = mem_add mem @@ uV SmthMV in let (mem, id2) = mem_add mem SmthV in
let (mem, id3) = mem_add mem @@ uV BotMV in let (mem, id3) = mem_add mem BotV in
Printf.printf "%i %i %i " id1 id2 id3; Printf.printf "%i %i %i " id1 id2 id3;
Printf.printf "%b %b %b " (v_memval_is (mem_get mem id1) ZeroMV) Printf.printf "%b %b %b " (mem_get mem id1 == ZeroV)
(v_memval_is (mem_get mem id2) SmthMV) (mem_get mem id2 == SmthV)
(v_memval_is (mem_get mem id3) BotMV); (mem_get mem id3 == BotV);
let mem = mem_set mem id1 @@ uV BotMV in let mem = mem_set mem id1 BotV in
let mem = mem_set mem id2 @@ uV ZeroMV in let mem = mem_set mem id2 ZeroV in
let mem = mem_set mem id3 @@ uV SmthMV in let mem = mem_set mem id3 SmthV in
Printf.printf "%b %b %b" (v_memval_is (mem_get mem id1) BotMV) Printf.printf "%b %b %b" (mem_get mem id1 == BotV)
(v_memval_is (mem_get mem id2) ZeroMV) (mem_get mem id2 == ZeroV)
(v_memval_is (mem_get mem id3) SmthMV); (mem_get mem id3 == SmthV);
[%expect {| 0 1 2 true true true true true true |}] [%expect {| 0 1 2 true true true true true true |}]
(* - basic var tests *) (* - basic var tests *)
@ -662,7 +555,7 @@ struct
ReadS (VarP globals_min_id)); ReadS (VarP globals_min_id));
[%expect.unreachable]); [%expect.unreachable]);
with Eval_error msg -> Printf.printf "%s" msg; with Eval_error msg -> Printf.printf "%s" msg;
[%expect {| memvmod: forbidden read |}] [%expect {| read: spoiled value |}]
let%expect_test "simple vars, no read & read" = let%expect_test "simple vars, no read & read" =
prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE); prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE);
@ -728,10 +621,10 @@ struct
let%expect_test "simple call with write, dsl" = let%expect_test "simple call with write, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defgu uT_aw; defgu uT_r_mw;
defg (rfT uT_aw) rfg0E; defg (rfT uT_r_mw) rfg0E;
FunD ( FunD (
[moded @@ cpT @@ uT_aw], [moded @@ cpT @@ uT_r_mw],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
) )
], ],
@ -743,10 +636,10 @@ struct
let%expect_test "simple call with read after write, dsl" = let%expect_test "simple call with read after write, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defgu uT_aw; defgu uT_r_mw;
defg (rfT uT_aw) rfg0E; defg (rfT uT_r_mw) rfg0E;
FunD ( FunD (
[moded @@ cpT @@ uT_aw], [moded @@ cpT @@ uT_mw],
(wrS @@ drf @@ v0) #. (wrS @@ drf @@ v0) #.
(rdS @@ drf @@ v0) (rdS @@ drf @@ v0)
) )
@ -803,7 +696,7 @@ struct
); );
[%expect.unreachable]); [%expect.unreachable]);
with Eval_error msg -> Printf.printf "%s" msg; with Eval_error msg -> Printf.printf "%s" msg;
[%expect {| memvmod: forbidden read |}] [%expect {| read: spoiled value |}]
let%expect_test "simple call with write to ref with fix, dsl" = let%expect_test "simple call with write to ref with fix, dsl" =
prog_eval_noret ( prog_eval_noret (
@ -886,9 +779,9 @@ struct
prog_eval_noret ( prog_eval_noret (
[ [
defgu uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r) rfg0E; defg (rfT uT_r_aw) rfg0E;
FunD ( FunD (
[moded @@ cpT @@ uT], [moded @@ cpT @@ uT_aw],
(wrS @@ vg0) #. (wrS @@ vg0) #.
(rdS @@ drf @@ vg1) (rdS @@ drf @@ vg1)
) )
@ -902,10 +795,10 @@ struct
let%expect_test "simple call with read & write (2 args), dsl" = let%expect_test "simple call with read & write (2 args), dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defgu uT_r; defgu uT_r_aw;
defg (rfT uT_r) rfg0E; defg (rfT uT_r_aw) rfg0E;
defgu uT_aw; defgu uT_r_aw;
defg (rfT uT_aw) rfg2E; defg (rfT uT_r_aw) rfg2E;
FunD ( FunD (
[ [
moded @@ rfT @@ uT_r; moded @@ rfT @@ uT_r;
@ -933,10 +826,10 @@ struct
defg (rfT uT_r_aw) rfg6E; defg (rfT uT_r_aw) rfg6E;
FunD ( FunD (
[ [
((NIn, NOut), cpT @@ uT); ((NIn, NOut), cpT @@ uT_aw);
((In, NOut), cpT @@ uT_r_aw); ((In, NOut), cpT @@ uT_r_aw);
((NIn, Out), rfT @@ uT_aw); ((NIn, Out), cpT @@ uT_aw);
((In, Out), rfT @@ uT_r_aw); ((In, Out), cpT @@ uT_r_aw);
], ],
(rdS @@ drf @@ v1) #. (rdS @@ drf @@ v1) #.
(rdS @@ drf @@ v3) #. (rdS @@ drf @@ v3) #.
@ -957,10 +850,10 @@ struct
let%expect_test "simple call with different arguments modifiers, ref, dsl" = let%expect_test "simple call with different arguments modifiers, ref, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defgu uT_r; defgu uT_r_aw;
defg (rfT uT_r) rfg0E; defg (rfT uT_r_aw) rfg0E;
defgu uT_r; defgu uT_r_aw;
defg (rfT uT_r) rfg2E; defg (rfT uT_r_aw) rfg2E;
defgu uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw) rfg4E; defg (rfT uT_r_aw) rfg4E;
defgu uT_r_aw; defgu uT_r_aw;
@ -989,82 +882,81 @@ struct
(* - complex tests *) (* - complex tests *)
(* TODO: FIXME: rw tags *)
(* NOTE: path access isreversed to intuitive function application (* NOTE: path access isreversed to intuitive function application
by definition *) by definition *)
(* let%expect_test "complex test: send, dsl" = *) let%expect_test "complex test: send, dsl" =
(* prog_eval_noret ( *) prog_eval_noret (
(* TODO: set optimal ref mods later *) (* TODO: set optimal ref mods later *)
(* let user_utilsT = TupleT [uT_r_aw (* 0 id *); uT_r_aw] in *) 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 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 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 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 utilsT = TupleT [uT_r_aw (* 0 has_version *); uT_r_aw (* 1 id *)] in
(* let requestT = TupleT [cpT userT (* 0 user *); *) let requestT = TupleT [cpT userT (* 0 user *);
(* cpT versionT (* 1 version *); *) cpT versionT (* 1 version *);
(* cpT utilsT (* 2 utils *); *) cpT utilsT (* 2 utils *);
(* cpT uT_r_aw (* 3 data *); *) cpT uT_r_aw (* 3 data *);
(* uT_r_aw (* 4 operation_date *)] in *) uT_r_aw (* 4 operation_date *)] in
(* let user_utilsE = TupleE [UnitE (* 0 id *); UnitE] in *) let user_utilsE = TupleE [UnitE (* 0 id *); UnitE] in
(* let user_infoE = TupleE [UnitE (* 0 name *); UnitE; UnitE] in *) let user_infoE = TupleE [UnitE (* 0 name *); UnitE; UnitE] in
(* let userE = TupleE [rfg0E (* 0 utils *); rfg1E (* 1 info *)] in *) let userE = TupleE [rfg0E (* 0 utils *); rfg1E (* 1 info *)] in
(* let versionE = TupleE [UnitE (* 0 id *); UnitE; UnitE] in *) let versionE = TupleE [UnitE (* 0 id *); UnitE; UnitE] in
(* let utilsE = TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] in *) let utilsE = TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] in
(* let requestE = TupleE [rfg2E (* 0 user *); *) let requestE = TupleE [rfg2E (* 0 user *);
(* rfg3E (* 1 version *); *) rfg3E (* 1 version *);
(* rfg4E (* 2 utils *); *) rfg4E (* 2 utils *);
(* rfg5E (* 3 data *); *) rfg5E (* 3 data *);
(* UnitE (* 4 operation_date *)] in *) UnitE (* 4 operation_date *)] in
(* let get_version_idID = vg7 in *) let get_version_idID = vg7 in
(* let updated_versionID = vg8 in *) let updated_versionID = vg8 in
(* let sendID = vg9 in *) let sendID = vg9 in
(* let send_allID = vg10 in *) let send_allID = vg10 in
(* let get_version_idF = FunD ([moded requestT], *) let get_version_idF = FunD ([moded requestT],
(* (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in *) (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in
(* let updated_versionF = FunD ([moded requestT], *) let updated_versionF = FunD ([moded requestT],
(* (rdS @@ access 0 @@ drf @@ access 2 v0) #. *) (rdS @@ access 0 @@ drf @@ access 2 v0) #.
(* TODO: read all the substructure ?? *) (* TODO: read all the substructure ?? *)
(* (rdS @@ access 0 @@ drf @@ access 1 v0) #. *) (rdS @@ access 0 @@ drf @@ access 1 v0) #.
(* (rdS @@ access 1 @@ drf @@ access 1 v0)) in *) (rdS @@ access 1 @@ drf @@ access 1 v0)) in
(* let sendF = FunD ([moded requestT], *) let sendF = FunD ([moded requestT],
(* (( *) ((
(* (wrS @@ access 0 @@ drf @@ access 2 v0) #. *) (wrS @@ access 0 @@ drf @@ access 2 v0) #.
(* (rdS @@ drf @@ access 3 v0) #. *) (rdS @@ drf @@ access 3 v0) #.
(* (wrS @@ drf @@ access 3 v0) #. *) (wrS @@ drf @@ access 3 v0) #.
(* (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0) *) (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0)
(* ) |. skp) #. *) ) |. skp) #.
(* (wrS @@ access 4 v0) #. *) (wrS @@ access 4 v0) #.
(* TODO: read all the substructure ?? *) (* TODO: read all the substructure ?? *)
(* (rdS @@ access 4 v0) (*rdS v0*)) in (* FIXME: TMP, parial read, should be full *) *) (rdS @@ access 4 v0) (*rdS v0*)) in (* FIXME: TMP, parial read, should be full *)
(* let send_allF = FunD ([moded requestT], *) let send_allF = FunD ([moded requestT],
(* (wrS @@ access 4 v0) (*wrS v0*) #. (* FIXME: TMP, parial write, should be full *) *) (wrS @@ access 4 v0) (*wrS v0*) #. (* FIXME: TMP, parial write, should be full *)
(* (callS sendID [pE v0]) #. *) (callS sendID [pE v0]) #.
(* (callS get_version_idID [pE v0]) #. *) (callS get_version_idID [pE v0]) #.
(* (callS updated_versionID [pE v0]) #. *) (callS updated_versionID [pE v0]) #.
(* TODO: read all the substructure ?? *) (* TODO: read all the substructure ?? *)
(* (wrS @@ access 0 @@ drf @@ access 1 v0) #. *) (wrS @@ access 0 @@ drf @@ access 1 v0) #.
(* (wrS @@ access 1 @@ drf @@ access 1 v0) #. *) (wrS @@ access 1 @@ drf @@ access 1 v0) #.
(* --- *) (* --- *)
(* ((rdS @@ access 0 @@ drf @@ access 0 @@ drf @@ access 0 v0) |. *) ((rdS @@ access 0 @@ drf @@ access 0 @@ drf @@ access 0 v0) |.
(* (rdS @@ access 0 @@ drf @@ access 1 v0))) in *) (rdS @@ access 0 @@ drf @@ access 1 v0))) in
(* let varID = vg6 in *) let varID = vg6 in
(* [ *) [
(* defg user_utilsT user_utilsE; *) defg user_utilsT user_utilsE;
(* defg user_infoT user_infoE; *) defg user_infoT user_infoE;
(* defg userT userE; *) defg userT userE;
(* defg versionT versionE; *) defg versionT versionE;
(* defg utilsT utilsE; *) defg utilsT utilsE;
(* defgu uT_r_aw; *) defgu uT_r_aw;
(* defg requestT requestE; *) defg requestT requestE;
(* get_version_idF; *) get_version_idF;
(* updated_versionF; *) updated_versionF;
(* sendF; *) sendF;
(* send_allF *) send_allF
(* ], *) ],
(* callS send_allID [pE varID] *) callS send_allID [pE varID]
(* ); *) );
(* Printf.printf "done!"; *) Printf.printf "done!";
(* [%expect {| done! |}] *) [%expect {| done! |}]
(* TODO: version with more optimal modifiers *) (* TODO: version with more optimal modifiers *)
end end

77
model_with_structures/model.typ
View file

@ -816,9 +816,9 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
$bot$, $0$, $?$, $bot$, $0$, $?$,
$bot$, $?$, $?$, $bot$, $?$, $?$,
// $bot$, $top$, $?$, // $bot$, $top$, $?$,
// $top$, $0$, $?$, $top$, $0$, $?$,
// $top$, $?$, $?$, $top$, $?$, $?$,
// $top$, $bot$, $?$, $top$, $bot$, $?$,
$bot$, $bot$, $bot$, $bot$, $bot$, $bot$,
// $top$, $top$, $top$, // $top$, $top$, $top$,
), ),
@ -942,7 +942,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
rule( rule(
name: [ unit expr value], name: [ unit expr value],
$vals, mu texpre () eqmu cdl 0_m, 0_r, 0_w cdr$, $vals, mu texpre () eqmu 0$,
) )
)) ))
@ -1064,7 +1064,6 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
#let spoil = `spoil` #let spoil = `spoil`
#let tryread = `try read` #let tryread = `try read`
#let tryspoil = `try spoil`
#let tcorrectnew = $attach(tack.r.double, br: #[correct])$ #let tcorrectnew = $attach(tack.r.double, br: #[correct])$
#align(center, prooftree( #align(center, prooftree(
@ -1106,44 +1105,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
) )
)) ))
#h(10pt) // TODO: extract correctness
#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) #h(10pt)
@ -1157,11 +1119,10 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
xarrowSquiggly(r)_tryread xarrowSquiggly(r)_tryread
cl v_m', v_r', v_w' cr$, cl v_m', v_r', v_w' cr$,
$v_m' modW writeA xarrowSquiggly(o \, AlwaysWrite)_tryspoil v_m''$, $w = AlwaysWrite$,
$cl cdl v_m, v_r, v_w cdr, mu cr $cl cdl v_m, v_r, v_w cdr, mu cr
xarrowSquiggly(cl r \, AlwaysWrite cr \, (\_, o) \, Ref)_spoil xarrowSquiggly(cl r \, w cr \, (\_, not Out) \, Ref)_spoil
cl cdl v_m'', v_r' modR writeA, v_w' modW writeA cdr, cdr, mu cr$, cl cdl bot, v_r' modR writeA, v_w' modW writeA cdr, cdr, mu cr$,
) )
)) ))
@ -1177,11 +1138,10 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
xarrowSquiggly(r)_tryread xarrowSquiggly(r)_tryread
cl v_m', v_r', v_w' cr$, cl v_m', v_r', v_w' cr$,
$v_m' modW mbwriteA xarrowSquiggly(o \, MaybeWrite)_tryspoil v_m''$, $w = MaybeWrite$,
$cl cdl v_m, v_r, v_w cdr, mu cr $cl cdl v_m, v_r, v_w cdr, mu cr
xarrowSquiggly(cl r \, MaybeWrite cr \, (\_, o) \, Ref)_spoil xarrowSquiggly(cl r \, w cr \, (\_, not Out) \, Ref)_spoil
cl cdl v_m'', v_r' modR mbwriteA, v_w' modW mbwriteA cdr, mu cr$, cl cdl ?, v_r' modR mbwriteA, v_w' modW mbwriteA cdr, mu cr$,
) )
)) ))
@ -1193,15 +1153,12 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
name: [ skip step], name: [ skip step],
$ tcorrectnew cl 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$,
$c = Copy or w = NotWrite$, $o == Out or c == Copy or w = NotWrite$,
$cl cdl v_m, v_r, v_w cdr, mu cr $cl cdl v_m, v_r, v_w cdr, mu cr
xarrowSquiggly(cl r \, w cr cr \, (\_, \_) \, c)_spoil xarrowSquiggly(cl r \, w cr cr \, (\_, o) \, c)_spoil
cl cdl v_m', v_r', v_w' cdr mu cr$, cl cdl v_m, v_r, v_w cdr mu cr$,
) )
)) ))
@ -1387,7 +1344,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
rule( rule(
name: [ lambda check], name: [ lambda check],
$mu ttags lambda space overline(s) :$, $mu ttags lambda overline(s) :$,
) )
)) ))
#align(center, prooftree( #align(center, prooftree(
@ -1436,9 +1393,9 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
cl types', vals', mu' cr$, cl types', vals', mu' cr$,
// NOTE: check that read and write tags are used properly // NOTE: check that read and write tags are used properly
$mu' ttags mu'[vals'[x_1]] : t_1$, $mu' ttags x_1 : t_1$,
$...$, $...$,
$mu' ttags mu'[vals'[x_n]] : t_n$, $mu' ttags x_n : t_n$,
$vals, mu_0 tfunceval cl s, [x_1, .. x_n], [t_1, ... t_n], [e_1, ... e_n] cr$, $vals, mu_0 tfunceval cl s, [x_1, .. x_n], [t_1, ... t_n], [e_1, ... e_n] cr$,
) )

371
model_with_structures/synthesizer.ml
View file

@ -164,44 +164,12 @@ struct
(* NOTE: deepvalue - not used (?) *) (* 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 module Value = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject [%%ocanren_inject
type nonrec ('vm, 'vr, 'vw, 'sl, 'd, 'vl) t = UnitV of 'vm * 'vr * 'vw type nonrec ('sl, 'd, 'vl) t = ZeroV | SmthV | BotV | FunV of 'sl | RefV of 'd | TupleV of 'vl
| FunV of 'sl
| RefV of 'd
| TupleV of 'vl
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type ground = (MemVal.ground, ReadVal.ground, WriteVal.ground, type ground = (((* Nat.ground List.ground * *) Stmt.ground) List.ground, Nat.ground, ground List.ground) t
((* Nat.ground List.ground * *) Stmt.ground) List.ground,
Nat.ground, ground List.ground) t
] ]
end end
@ -214,15 +182,6 @@ struct
] ]
end 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 module MemEnv = struct
@ -381,17 +340,6 @@ struct
{ xs == [] & ys == [] & zs == [] } { 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 *) (* - state utils *)
let types_assoco id types tp = let types_assoco id types tp =
@ -511,8 +459,7 @@ struct
let is_trivial_vo v = let is_trivial_vo v =
let open Value in let open Value in
ocanren { ocanren {
fresh v_m, v_r, v_w in v == ZeroV | v == SmthV | v == BotV
v == UnitV (v_m, v_r, v_w)
} }
let rec pathvaro p x = let rec pathvaro p x =
@ -593,19 +540,12 @@ struct
let open Value in let open Value in
let open ReadCap 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 { ocanren {
{ fresh r, w in { fresh r, w in
is_trivial_vo v & is_trivial_vo v &
tp == UnitT (r, w) & tp == UnitT (r, w) &
{ { fresh v_m, _v_r, _v_w in { { r == Rd & mem_with_id' == Std.pair mem v } |
r == Rd & { r == NRd & mem_with_id' == Std.pair mem BotV } } } |
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 { fresh stmts, ts in
v == FunV stmts & v == FunV stmts &
tp == FunT ts & tp == FunT ts &
@ -627,43 +567,10 @@ struct
mem_with_id' == Std.pair mem' (TupleV vs') } 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 *) (* - value update *)
(* NOTE: reversed path used *) (* NOTE: reversed path used *)
let rec valchangeo mem v rp b mem_with_v' = let rec valupdo mem v rp b mem_with_v' =
let open RevPath in let open RevPath in
let open Value in let open Value in
ocanren { ocanren {
@ -673,7 +580,7 @@ struct
rp == DerefRP rp' & rp == DerefRP rp' &
v == RefV id & v == RefV id &
mem_geto mem id v' & mem_geto mem id v' &
valchangeo mem v' rp' b mem_with_v_upd & valupdo mem v' rp' b mem_with_v_upd &
Std.pair mem_upd v_upd == mem_with_v_upd & Std.pair mem_upd v_upd == mem_with_v_upd &
mem_seto mem_upd id v_upd mem_st & mem_seto mem_upd id v_upd mem_st &
mem_with_v' == Std.pair mem_st (RefV id) } | mem_with_v' == Std.pair mem_st (RefV id) } |
@ -681,40 +588,7 @@ struct
rp == AccessRP (rp', id) & rp == AccessRP (rp', id) &
v == TupleV vs' & v == TupleV vs' &
list_ntho vs' id v' & list_ntho vs' id v' &
valchangeo mem v' rp' b mem_with_v_upd & valupdo mem v' rp' b mem_with_v_upd &
Std.pair mem_upd v_upd == mem_with_v_upd &
list_replaceo vs' id v_upd vs_upd &
mem_with_v' == Std.pair mem_upd (TupleV vs_upd) }
}
(* 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 & Std.pair mem_upd v_upd == mem_with_v_upd &
list_replaceo vs' id v_upd vs_upd & list_replaceo vs' id v_upd vs_upd &
mem_with_v' == Std.pair mem_upd (TupleV vs_upd) } mem_with_v' == Std.pair mem_upd (TupleV vs_upd) }
@ -722,50 +596,13 @@ struct
(* - value combination *) (* - 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 & v =/= ZeroMV &
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 & v =/= ZeroWV &
u =/= OneWV & v =/= OneWV &
u' == SmthWV }
}
let rec valcombo u v u' = let rec valcombo u v u' =
let open Value in let open Value in
ocanren { ocanren {
{ fresh u_m, u_r, u_w, { is_trivial_vo u &
v_m, v_r, v_w, is_trivial_vo v &
u_m', u_r', u_w' in (* TODO: do not use disequality constraint ? *)
u == UnitV (u_m, u_r, u_w) & { { u == v & u' == u } | { u =/= v & u' == BotV } } } |
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 { fresh ustmts, vstmts, ustmts' in
u == FunV ustmts & u == FunV ustmts &
v == FunV vstmts & v == FunV vstmts &
@ -805,11 +642,8 @@ struct
exprvalo mem vals e v' = exprvalo mem vals e v' =
let open Expr in let open Expr in
let open Value in let open Value in
let open MemVal in
let open ReadVal in
let open WriteVal in
ocanren { ocanren {
{ e == UnitE & v' == UnitV (ZeroMV, ZeroRV, ZeroWV) } | { e == UnitE & v' == ZeroV } |
{ fresh p in { fresh p in
e == PathE p & e == PathE p &
pathvalo mem vals p v' } | pathvalo mem vals p v' } |
@ -926,99 +760,76 @@ struct
(* - call values spoil *) (* - call values spoil *)
(* TODO: check that negation is interpreted correctly *) (* TODO: check that negation is interpreted correctly *)
let is_correct_tagso r w m c = let is_correct_tagso v r w _r' w' m c =
let open Value in
let open ReadCap in let open ReadCap in
let open WriteCap in let open WriteCap in
let open Mode in let open Mode in
let open CopyCap in let open CopyCap in
ocanren { ocanren {
{ r == NRd | r == Rd & v == ZeroV } &
{ r == NRd | r == Rd & is_ino m } & { r == NRd | r == Rd & is_ino m } &
{ is_not_outo m | is_outo m & w == AlwaysWr & c == Rf } { 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
} }
let tryreado r v_m v_r v_w v' = let rec valspoil_foldero m c mem_with_vs tp u v mem_with_vs' = ocanren {
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 MemVal in
ocanren {
{ 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 fresh mem, vs, mem', v' in
Std.pair mem vs == mem_with_vs & Std.pair mem vs == mem_with_vs &
valspoilo mem v tp m c (Std.pair mem' v') & valspoilo mem v tp u m c (Std.pair mem' v') &
mem_with_vs' == Std.pair mem' (v' :: vs) mem_with_vs' == Std.pair mem' (v' :: vs)
} }
and valspoilo mem v tp m c mem_with_v' = and valspoilo mem v tp u m c mem_with_v' =
let open Type in let open Type in
let open Value in let open Value in
let open Mode in let open Mode in
let open WriteCap in let open WriteCap in
let open CopyCap in let open CopyCap in
let open Action in
ocanren { ocanren {
{ fresh r, w, { fresh r, w, r', w' in
v_m, v_r, v_w,
v', v'' in
tp == UnitT (r, w) & tp == UnitT (r, w) &
v == UnitV (v_m, v_r, v_w) & u == UnitT (r', w') &
is_correct_tagso r w m c & is_trivial_vo v &
tryreado r v_m v_r v_w v' & is_correct_tagso v r w r' w' m c &
{ {
{ c == Cp & w == NeverWr & { is_not_outo m &
mem_with_v' == Std.pair mem v' } | c == Rf &
{ fresh v_m', v_r', v_w', { w == AlwaysWr | w == MayWr } &
v_m'', v_r'', v_w'', mem_with_v' == Std.pair mem BotV } |
v_m''' in { is_outo m &
v' == UnitV (v_m', v_r', v_w') & w == AlwaysWr &
{ mem_with_v' == Std.pair mem ZeroV } |
{ w == AlwaysWr & { { is_outo m |
memvmodo AlwaysWriteA v_m' v_m'' & is_not_outo m & c == Cp |
readvmodo AlwaysWriteA v_r' v_r'' & is_not_outo m & c == Rf & w == NeverWr } &
writevmodo AlwaysWriteA v_w' v_w'' } | { is_not_outo m |
{ w == MayWr & is_outo m & w == MayWr |
memvmodo MayWriteA v_m' v_m'' & is_outo m & w == NeverWr } &
readvmodo MayWriteA v_r' v_r'' & mem_with_v' == Std.pair mem v }
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, _stmts in { fresh ts, us, _stmts in
tp == FunT ts & tp == FunT ts &
u == FunT us &
v == FunV _stmts & v == FunV _stmts &
ts == us &
mem_with_v' == Std.pair mem v } | mem_with_v' == Std.pair mem v } |
{ fresh ctp', tp', cu', id', v', mem_sp, v_sp, mem_set in { fresh ctp', tp', cu', u', id', v', mem_sp, v_sp, mem_set in
tp == RefT (ctp', tp') & tp == RefT (ctp', tp') &
u == RefT (cu', u') &
v == RefV id' & v == RefV id' &
mem_geto mem id' v' & mem_geto mem id' v' &
valspoilo mem v' tp' m ctp' (Std.pair mem_sp v_sp) & valspoilo mem v' tp' u' m ctp' (Std.pair mem_sp v_sp) &
mem_seto mem_sp id' v_sp mem_set & mem_seto mem_sp id' v_sp mem_set &
mem_with_v' == Std.pair mem_set (RefV id') } | mem_with_v' == Std.pair mem_set (RefV id') } |
{ fresh tps, us, vs, mem_sp, vs_sp in { fresh tps, us, vs, mem_sp, vs_sp in
tp == TupleT tps & tp == TupleT tps &
u == TupleT us &
v == TupleV vs & v == TupleV vs &
list_foldr2o (valspoil_foldero m c) list_foldr3o (valspoil_foldero m c)
(Std.pair mem []) tps vs (Std.pair mem []) tps us vs
(Std.pair mem_sp vs_sp) & (Std.pair mem_sp vs_sp) &
mem_with_v' == Std.pair mem_sp (TupleV vs_sp) mem_with_v' == Std.pair mem_sp (TupleV vs_sp)
} }
@ -1032,17 +843,17 @@ struct
let open RevPath in let open RevPath in
ocanren { ocanren {
fresh mem, types, vals, visited, 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 mem_sp, b_sp, v_sp, mem_upd, v_upd in
st == StEnv (mem, types, vals, visited) & st == StEnv (mem, types, vals, visited) &
pathvaro p x & pathvaro p x &
vals_assoco x vals id & vals_assoco x vals id &
pathvalo mem vals p b & pathvalo mem vals p b &
(* pathtypeo types p tp' & *) pathtypeo types p tp' &
valspoilo mem b tp tp' m Cp (Std.pair mem_sp b_sp) & valspoilo mem b tp tp' m Cp (Std.pair mem_sp b_sp) &
mem_geto mem_sp id v_sp & mem_geto mem_sp id v_sp &
pathrevo p VarRP rp & pathrevo p VarRP rp &
valchangeo mem_sp v_sp rp b_sp (Std.pair mem_upd v_upd) & valupdo mem_sp v_sp rp b_sp (Std.pair mem_upd v_upd) &
mem_seto mem_upd id v_upd mem' mem_seto mem_upd id v_upd mem'
} }
@ -1099,45 +910,8 @@ struct
(* - function evaluation *) (* - function evaluation *)
(* NOTE: not needed due to performed optimization in stmt_eval ? *) (* 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 == R & v_r == OneRV } |
{ r == NRd & v_r == ZeroRV } |
{ r == NRd & v_r == TopRV }
} &
writeval_to_vapo 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, ts in
List.mapo (tags_checko mem) vs ts }
}
(* - statement evaluation *) (* - statement evaluation *)
(* TODO *)
let rec stmt_addarg_foldero vals st_with_id mtp e st_with_id' = ocanren { let rec stmt_addarg_foldero vals st_with_id mtp e st_with_id' = ocanren {
fresh st, x, m, tp, st' in fresh st, x, m, tp, st' in
@ -1146,26 +920,16 @@ struct
addargo st vals x tp e st' & addargo st vals x tp e st' &
st_with_id' == Std.pair st' (Nat.s x) st_with_id' == Std.pair st' (Nat.s x)
} }
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 visited stmt visited' = and stmt_eval_func_foldero mem types vals visited stmt visited' =
let open StEnv in let open StEnv in
ocanren { ocanren {
{ fresh visited_add, st, { fresh visited_add, st,
st', mem', types', vals', st', mem', types', vals' in
_x' in
not_visited_checko visited stmt & not_visited_checko visited stmt &
visited_addo visited stmt visited_add & visited_addo visited stmt visited_add &
st == StEnv (mem, types, vals, visited_add) & st == StEnv (mem, types, vals, visited_add) &
stmt_evalo st stmt st' & 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 ts _x' } |
{ visited_checko visited stmt & { visited_checko visited stmt &
visited == visited' } visited == visited' }
} }
@ -1186,7 +950,6 @@ struct
let open TypesEnv in let open TypesEnv in
let open ValsEnv in let open ValsEnv in
let open RevPath in let open RevPath in
let open Action in
ocanren { ocanren {
fresh mem, types, vals, visited in fresh mem, types, vals, visited in
st == StEnv (mem, types, vals, visited) & st == StEnv (mem, types, vals, visited) &
@ -1232,25 +995,13 @@ struct
vals_assoco x vals id & vals_assoco x vals id &
mem_geto mem id v & mem_geto mem id v &
pathrevo p VarRP rp & pathrevo p VarRP rp &
valupdo mem v rp AlwaysWriteA (Std.pair mem_upd v_upd) & valupdo mem v rp ZeroV (Std.pair mem_upd v_upd) &
mem_seto mem_upd id v_upd mem_set & mem_seto mem_upd id v_upd mem_set &
st' == StEnv (mem_set, types, vals, visited) } | st' == StEnv (mem_set, types, vals, visited) } |
{ fresh p, tp, _r, _w, x, id, v, rp, { fresh p in
mem_upd, v_upd, mem_set in
s == ReadS p & s == ReadS p &
pathtypeo types p tp & pathvalo mem vals p ZeroV &
tp == UnitT (_r, _w) & st == st' } |
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 { fresh sl, sr, stl in
s == SeqS (sl, sr) & s == SeqS (sl, sr) &
stmt_evalo st sl stl & stmt_evalo st sl stl &