mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-06-10 19:28:16 +00:00
struct: fox spoil in root: use copy capability Cp
This commit is contained in:
ProgramSnail
parent
bd809ed1cf
commit
547d419b48
3 changed files with 103 additions and 16 deletions
|
|
@ -323,11 +323,12 @@ struct
|
|||
let argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem =
|
||||
match state with (mem, types, vals) ->
|
||||
let x = pathvar p in
|
||||
let id = vals_assoc x vals in
|
||||
let b = pathval mem vals p in
|
||||
let t' = pathtype types p in
|
||||
let (mem', b') = valspoil mem b t t' m Rf in
|
||||
let (mem'', v'') = valupd mem' (mem_get mem' id) p b' 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 *)
|
||||
(* TODO: FIXME: why copy (Cp)? *)
|
||||
let (mem'', v'') = valupd mem' (mem_get mem' id) p b' in (* set subvalue into var *)
|
||||
mem_set mem'' id v''
|
||||
|
||||
let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem =
|
||||
|
|
@ -394,8 +395,10 @@ struct
|
|||
let (mem', v') = valupd mem (mem_get mem id) p ZeroV in
|
||||
(mem_set mem' id v', types, vals)
|
||||
| _ -> raise @@ Eval_error "write: type")
|
||||
| ReadS p -> if pathval mem vals p != ZeroV
|
||||
then raise @@ Eval_error "read"
|
||||
| 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
|
||||
| SeqS (sl, sr) -> let statel = stmt_eval state sl in
|
||||
stmt_eval statel sr
|
||||
|
|
@ -429,12 +432,18 @@ struct
|
|||
let v3 = VarP 3
|
||||
let v4 = VarP 4
|
||||
let v5 = VarP 5
|
||||
let vg0 = VarP (globals_min_id)
|
||||
let v6 = VarP 6
|
||||
let v7 = VarP 7
|
||||
let v8 = VarP 8
|
||||
let vg0 = VarP globals_min_id
|
||||
let vg1 = VarP (globals_min_id + 1)
|
||||
let vg2 = VarP (globals_min_id + 2)
|
||||
let vg3 = VarP (globals_min_id + 3)
|
||||
let vg4 = VarP (globals_min_id + 4)
|
||||
let vg5 = VarP (globals_min_id + 5)
|
||||
let vg6 = VarP (globals_min_id + 6)
|
||||
let vg7 = VarP (globals_min_id + 7)
|
||||
let vg8 = VarP (globals_min_id + 8)
|
||||
|
||||
let rf0E = RefE 0
|
||||
let rf1E = RefE 1
|
||||
|
|
@ -442,12 +451,19 @@ struct
|
|||
let rf3E = RefE 3
|
||||
let rf4E = RefE 4
|
||||
let rf5E = RefE 5
|
||||
let rf3E = RefE 3
|
||||
let rf4E = RefE 4
|
||||
let rf5E = RefE 5
|
||||
let rfg0E = RefE globals_min_id
|
||||
let rfg1E = RefE (globals_min_id + 1)
|
||||
let rfg2E = RefE (globals_min_id + 2)
|
||||
let rfg3E = RefE (globals_min_id + 3)
|
||||
let rfg4E = RefE (globals_min_id + 4)
|
||||
let rfg5E = RefE (globals_min_id + 5)
|
||||
let rfg6E = RefE (globals_min_id + 6)
|
||||
let rfg7E = RefE (globals_min_id + 7)
|
||||
let rfg8E = RefE (globals_min_id + 8)
|
||||
|
||||
let pE p = PathE p
|
||||
|
||||
let drf p = DerefP p
|
||||
|
|
@ -511,7 +527,7 @@ struct
|
|||
try(prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], ReadS (VarP globals_min_id));
|
||||
[%expect.unreachable]);
|
||||
with Eval_error msg -> Printf.printf "%s" msg;
|
||||
[%expect {| read |}]
|
||||
[%expect {| read: spoiled value |}]
|
||||
|
||||
let%expect_test "simple vars, no read & read" =
|
||||
prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE);
|
||||
|
|
@ -649,7 +665,7 @@ struct
|
|||
);
|
||||
[%expect.unreachable]);
|
||||
with Eval_error msg -> Printf.printf "%s" msg;
|
||||
[%expect {| read |}]
|
||||
[%expect {| read: spoiled value |}]
|
||||
|
||||
let%expect_test "call inside call, dsl" =
|
||||
prog_eval_noret (
|
||||
|
|
@ -695,7 +711,7 @@ struct
|
|||
defgu uT_r_aw;
|
||||
defg (rfT uT_r_aw) rfg0E;
|
||||
defgu uT_r_aw;
|
||||
defg (rfT uT_r_aw) rfg0E;
|
||||
defg (rfT uT_r_aw) rfg2E;
|
||||
FunD (
|
||||
[
|
||||
moded @@ rfT @@ uT_r;
|
||||
|
|
@ -710,6 +726,76 @@ struct
|
|||
Printf.printf "done!";
|
||||
[%expect {| done! |}]
|
||||
|
||||
let%expect_test "simple call with different arguments modifiers, copy, 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_aw;
|
||||
defg (rfT uT_r_aw) rfg4E;
|
||||
defgu uT_r_aw;
|
||||
defg (rfT uT_r_aw) rfg6E;
|
||||
FunD (
|
||||
[
|
||||
((NIn, NOut), cpT @@ uT_aw);
|
||||
((In, NOut), cpT @@ uT_r_aw);
|
||||
((NIn, Out), cpT @@ uT_aw);
|
||||
((In, Out), cpT @@ uT_r_aw);
|
||||
],
|
||||
(rdS @@ drf @@ v1) #.
|
||||
(rdS @@ drf @@ v3) #.
|
||||
(wrS @@ drf @@ v1) #.
|
||||
(wrS @@ drf @@ v2) #.
|
||||
(wrS @@ drf @@ v3)
|
||||
)
|
||||
],
|
||||
(callS vg8 [pE vg1; pE vg3; pE vg5; pE vg7]) #.
|
||||
(rdS @@ drf @@ vg1) #.
|
||||
(rdS @@ drf @@ vg3) #.
|
||||
(rdS @@ drf @@ vg5) #.
|
||||
(rdS @@ drf @@ vg7)
|
||||
);
|
||||
Printf.printf "done!";
|
||||
[%expect {| done! |}]
|
||||
|
||||
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_aw;
|
||||
defg (rfT uT_r_aw) rfg4E;
|
||||
defgu uT_r_aw;
|
||||
defg (rfT uT_r_aw) rfg6E;
|
||||
FunD (
|
||||
[
|
||||
((NIn, NOut), rfT @@ uT);
|
||||
((In, NOut), rfT @@ uT_r);
|
||||
((NIn, Out), rfT @@ uT_aw);
|
||||
((In, Out), rfT @@ uT_r_aw);
|
||||
],
|
||||
(rdS @@ drf @@ v1) #.
|
||||
(rdS @@ drf @@ v3) #.
|
||||
(wrS @@ drf @@ v2) #.
|
||||
(wrS @@ drf @@ v3)
|
||||
)
|
||||
],
|
||||
(callS vg8 [pE vg1; pE vg3; pE vg5; pE vg7]) #.
|
||||
(rdS @@ drf @@ vg1) #.
|
||||
(rdS @@ drf @@ vg3) #.
|
||||
(rdS @@ drf @@ vg5) #.
|
||||
(rdS @@ drf @@ vg7)
|
||||
);
|
||||
Printf.printf "done!";
|
||||
[%expect {| done! |}]
|
||||
|
||||
(* TODO: call after call test (fix test) *)
|
||||
(* TODO: recursive call test (for the future when memoization will be implemented) *)
|
||||
|
||||
(* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
|
||||
|
||||
(* --- tests --- *)
|
||||
|
|
|
|||
|
|
@ -906,9 +906,10 @@ $s in stmt, f in X, x in X, a in X$
|
|||
$l = vals[x]$,
|
||||
$vals, mu texpre p eqmu b$,
|
||||
$types ttype p : t'$,
|
||||
// TODO: FIXME: Ref or Copy ?? in root <- Ref ??, because otherwise there could not b any Refs
|
||||
// TODO: FIXME: Ref or Copy ?? in root <- Copy ??,
|
||||
// <- otherwise all subsequent copy capabilities will be ref (in current impl)
|
||||
// FIXME depends on parent ??
|
||||
$cl b, mu cr xarrowSquiggly(t \, t' \, m \, Ref)_spoil cl b', mu' cr$,
|
||||
$cl b, mu cr xarrowSquiggly(t \, t' \, m \, Copy)_spoil cl b', mu' cr$,
|
||||
$cl mu'[l], mu' cr xarrowSquiggly(cl p \, b' cr)_modify cl v'', mu'' cr$,
|
||||
|
||||
$mu stretch(=>)^(m space t space p)_(cl vals, types cr) mu''[l <- v'']$,
|
||||
|
|
@ -920,7 +921,7 @@ $s in stmt, f in X, x in X, a in X$
|
|||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ full spoil for tuple expr],
|
||||
name: [ full spoil for ref expr],
|
||||
|
||||
// NOTE: x as path
|
||||
$mu stretch(=>)^(m space t space x)_(cl vals, types cr) mu'$,
|
||||
|
|
@ -941,7 +942,7 @@ $s in stmt, f in X, x in X, a in X$
|
|||
$...$,
|
||||
$mu_(n - 1) stretch(=>)^(m space t_n space e_n)_(cl vals, types cr) mu_n$,
|
||||
|
||||
$mu_0 stretch(=>)^(m space [t_1, ... t_n] space [e_1, ... e_n]_(cl vals, types cr) mu_n$,
|
||||
$mu_0 stretch(=>)^(m space [t_1, ... t_n] space [e_1, ... e_n])_(cl vals, types cr) mu_n$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
|
|||
|
|
@ -717,7 +717,7 @@ struct
|
|||
vals_assoco x vals id &
|
||||
pathvalo mem vals p b &
|
||||
pathtypeo types p tp' &
|
||||
valspoilo mem b tp tp' m Rf(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 &
|
||||
valupdo mem_sp v_sp p b_sp (Std.pair mem_upd v_upd) &
|
||||
mem_seto mem_upd id v_upd mem'
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue