st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-06-10 19:28:16 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

struct: analyzer fixes (except tags fix for complex test)

Browse source
This commit is contained in:
ProgramSnail 2026-05-13 16:55:15 +00:00
parent 60da9bdb3f
commit 5f55e3ecee
1 changed files with 118 additions and 108 deletions
Download patch file Download diff file Expand all files Collapse all files

226
model_with_structures/analyzer.ml
View file

@ -215,7 +215,7 @@ struct
let memvmod (a : action) (v_m : memval) : memval = let memvmod (a : action) (v_m : memval) : memval =
match a, v_m with match a, v_m with
| ReadA, ZeroMV -> ZeroMV | ReadA, ZeroMV -> ZeroMV
| ReadA, _ -> raise @@ Typing_error "memvmod: forbidden read" | ReadA, _ -> raise @@ Eval_error "memvmod: forbidden read"
| AlwaysWriteA, _ -> ZeroMV | AlwaysWriteA, _ -> ZeroMV
| MayWriteA, ZeroMV -> ZeroMV | MayWriteA, ZeroMV -> ZeroMV
| MayWriteA, _ -> SmthMV | MayWriteA, _ -> SmthMV
@ -364,7 +364,7 @@ struct
: mem * value = match t, v with : mem * value = match t, v with
| UnitT (r, w), UnitV (v_m, v_r, v_w) -> | UnitT (r, w), UnitV (v_m, v_r, v_w) ->
if not @@ is_correct_tags r w m c if not @@ is_correct_tags r w m c
then raise @@ Typing_error "valspoil: unit, not correct" then raise @@ Typing_error "valspoil: trivial type tags combination is not correct"
else else
let v' = tryread r v_m v_r v_w in let v' = tryread r v_m v_r v_w in
if c == Cp || w == NeverWr if c == Cp || w == NeverWr
@ -443,8 +443,10 @@ struct
let rec tags_check (mem : mem) (v : value) (t : atype) : unit = let rec tags_check (mem : mem) (v : value) (t : atype) : unit =
match v, t with match v, t with
| UnitV (v_m, v_r, v_w), UnitT (r, w) -> | UnitV (v_m, v_r, v_w), UnitT (r, w) ->
if (r == Rd) != (v_r == OneRV) if (r == Rd) && (v_r != OneRV)
then raise @@ Eval_error "tags_check: wrong read tag" 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 else if writeval_to_cap v_w != w
then raise @@ Eval_error "tags_check: wrong write tag" then raise @@ Eval_error "tags_check: wrong write tag"
else () else ()
@ -477,12 +479,12 @@ struct
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) -> (mem_after_stmt, _, vals_after_stmt, visited_after_stmt) ->
ignore @@ List.fold_right ignore @@ List.fold_left
(fun (_, t) x -> (fun x (_, t) ->
let id = vals_assoc x vals_after_stmt in let id = vals_assoc x vals_after_stmt in
let v = mem_get mem_after_stmt id in let v = mem_get mem_after_stmt id in
tags_check mem_after_stmt v t; x + 1) tags_check mem_after_stmt v t; x + 1)
ts 0; 0 ts;
visited_after_stmt) visited_after_stmt)
visited_swa visited_swa
fstmts in fstmts in
@ -508,13 +510,15 @@ struct
| _ -> raise @@ Eval_error "write: type") | _ -> raise @@ Eval_error "write: type")
| ReadS p -> (match pathtype types p with | ReadS p -> (match pathtype types p with
| UnitT (r, _) -> | UnitT (r, _) ->
if r == NRd (* NOTE: not required *)
then raise @@ Eval_error "read: write tag" (* if r == NRd *)
else let x = pathvar p in (* then raise @@ Eval_error "read: not read tag" *)
let id = vals_assoc x vals in (* else *)
let pi = pathrev p VarRP in let x = pathvar p in
let (mem', v') = valupd mem (mem_get mem id) pi ReadA in let id = vals_assoc x vals in
(mem_set mem' id v', types, vals, visited) 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" | RefT _ -> raise @@ Eval_error "read: ref type"
| TupleT _ -> raise @@ Eval_error "read: tuple type" | TupleT _ -> raise @@ Eval_error "read: tuple type"
| _ -> raise @@ Eval_error "read: type") | _ -> raise @@ Eval_error "read: type")
@ -621,21 +625,26 @@ struct
(* - 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 @@ uV ZeroMV in
let (mem, id2) = mem_add mem @@ uV SmthMV in let (mem, id2) = mem_add mem @@ uV SmthMV in
let (mem, id3) = mem_add mem @@ uV BotMV in let (mem, id3) = mem_add mem @@ uV BotMV in
Printf.printf "%i %i %i " id1 id2 id3; Printf.printf "%i %i %i " id1 id2 id3;
Printf.printf "%b %b %b " (mem_get mem id1 == uV ZeroMV) Printf.printf "%b %b %b " (v_memval_is (mem_get mem id1) ZeroMV)
(mem_get mem id2 == uV SmthMV) (v_memval_is (mem_get mem id2) SmthMV)
(mem_get mem id3 == uV BotMV); (v_memval_is (mem_get mem id3) BotMV);
let mem = mem_set mem id1 @@ uV BotMV in let mem = mem_set mem id1 @@ uV BotMV in
let mem = mem_set mem id2 @@ uV ZeroMV in let mem = mem_set mem id2 @@ uV ZeroMV in
let mem = mem_set mem id3 @@ uV SmthMV in let mem = mem_set mem id3 @@ uV SmthMV in
Printf.printf "%b %b %b" (mem_get mem id1 == uV BotMV) Printf.printf "%b %b %b" (v_memval_is (mem_get mem id1) BotMV)
(mem_get mem id2 == uV ZeroMV) (v_memval_is (mem_get mem id2) ZeroMV)
(mem_get mem id3 == uV SmthMV); (v_memval_is (mem_get mem id3) SmthMV);
[%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 *)
@ -656,7 +665,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 {| read: spoiled value |}] [%expect {| memvmod: forbidden read |}]
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);
@ -722,10 +731,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_r_mw; defgu uT_aw;
defg (rfT uT_r_mw) rfg0E; defg (rfT uT_aw) rfg0E;
FunD ( FunD (
[moded @@ cpT @@ uT_r_mw], [moded @@ cpT @@ uT_aw],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
) )
], ],
@ -737,10 +746,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_r_mw; defgu uT_aw;
defg (rfT uT_r_mw) rfg0E; defg (rfT uT_aw) rfg0E;
FunD ( FunD (
[moded @@ cpT @@ uT_mw], [moded @@ cpT @@ uT_aw],
(wrS @@ drf @@ v0) #. (wrS @@ drf @@ v0) #.
(rdS @@ drf @@ v0) (rdS @@ drf @@ v0)
) )
@ -797,7 +806,7 @@ struct
); );
[%expect.unreachable]); [%expect.unreachable]);
with Eval_error msg -> Printf.printf "%s" msg; 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" = let%expect_test "simple call with write to ref with fix, dsl" =
prog_eval_noret ( prog_eval_noret (
@ -880,9 +889,9 @@ struct
prog_eval_noret ( prog_eval_noret (
[ [
defgu uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw) rfg0E; defg (rfT uT_r) rfg0E;
FunD ( FunD (
[moded @@ cpT @@ uT_aw], [moded @@ cpT @@ uT],
(wrS @@ vg0) #. (wrS @@ vg0) #.
(rdS @@ drf @@ vg1) (rdS @@ drf @@ vg1)
) )
@ -896,10 +905,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_aw; defgu uT_r;
defg (rfT uT_r_aw) rfg0E; defg (rfT uT_r) rfg0E;
defgu uT_r_aw; defgu uT_aw;
defg (rfT uT_r_aw) rfg2E; defg (rfT uT_aw) rfg2E;
FunD ( FunD (
[ [
moded @@ rfT @@ uT_r; moded @@ rfT @@ uT_r;
@ -927,10 +936,10 @@ struct
defg (rfT uT_r_aw) rfg6E; defg (rfT uT_r_aw) rfg6E;
FunD ( FunD (
[ [
((NIn, NOut), cpT @@ uT_aw); ((NIn, NOut), cpT @@ uT);
((In, NOut), cpT @@ uT_r_aw); ((In, NOut), cpT @@ uT_r_aw);
((NIn, Out), cpT @@ uT_aw); ((NIn, Out), rfT @@ uT_aw);
((In, Out), cpT @@ uT_r_aw); ((In, Out), rfT @@ uT_r_aw);
], ],
(rdS @@ drf @@ v1) #. (rdS @@ drf @@ v1) #.
(rdS @@ drf @@ v3) #. (rdS @@ drf @@ v3) #.
@ -951,10 +960,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_aw; defgu uT_r;
defg (rfT uT_r_aw) rfg0E; defg (rfT uT_r) rfg0E;
defgu uT_r_aw; defgu uT_r;
defg (rfT uT_r_aw) rfg2E; defg (rfT uT_r) 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;
@ -983,81 +992,82 @@ 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