From 5f55e3ecee2306b3111e90b4f04134ec611a55a7 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Wed, 13 May 2026 16:55:15 +0000 Subject: [PATCH] struct: analyzer fixes (except tags fix for complex test) --- model_with_structures/analyzer.ml | 226 ++++++++++++++++-------------- 1 file changed, 118 insertions(+), 108 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 87e50fa..0d3c5c3 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -215,7 +215,7 @@ struct let memvmod (a : action) (v_m : memval) : memval = match a, v_m with | ReadA, ZeroMV -> ZeroMV - | ReadA, _ -> raise @@ Typing_error "memvmod: forbidden read" + | ReadA, _ -> raise @@ Eval_error "memvmod: forbidden read" | AlwaysWriteA, _ -> ZeroMV | MayWriteA, ZeroMV -> ZeroMV | MayWriteA, _ -> SmthMV @@ -364,7 +364,7 @@ struct : 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: unit, not correct" + 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 @@ -443,8 +443,10 @@ struct 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) + 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 () @@ -477,12 +479,12 @@ struct then stmt :: visited_old else match stmt_eval (mem_swa, types_swa, vals_swa, stmt :: visited_old) stmt with (mem_after_stmt, _, vals_after_stmt, visited_after_stmt) -> - ignore @@ List.fold_right - (fun (_, t) x -> + 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) - ts 0; + 0 ts; visited_after_stmt) visited_swa fstmts in @@ -508,13 +510,15 @@ struct | _ -> raise @@ Eval_error "write: type") | ReadS p -> (match pathtype types p with | UnitT (r, _) -> - if r == NRd - then raise @@ Eval_error "read: write 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) + (* 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") @@ -621,21 +625,26 @@ struct (* - 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 @@ 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 == uV ZeroMV) - (mem_get mem id2 == uV SmthMV) - (mem_get mem id3 == uV BotMV); + 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" (mem_get mem id1 == uV BotMV) - (mem_get mem id2 == uV ZeroMV) - (mem_get mem id3 == uV SmthMV); + 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 *) @@ -656,7 +665,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); @@ -722,10 +731,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 ) ], @@ -737,10 +746,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) ) @@ -797,7 +806,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 ( @@ -880,9 +889,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) ) @@ -896,10 +905,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; @@ -927,10 +936,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) #. @@ -951,10 +960,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; @@ -983,81 +992,82 @@ struct (* - 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 ( + (* 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) #. + (* let user_utilsT = TupleT [uT_r_aw (* 0 id *); uT_r_aw] in *) + (* let user_infoT = TupleT [uT_r_aw (* 0 name *); uT_r_aw; uT_r_aw] in *) + (* let userT = TupleT [cpT user_utilsT (* 0 utils *); cpT user_infoT (* 1 info *)] in *) + (* let versionT = TupleT [uT_r_aw (* 0 id *); uT_r_aw; uT_r_aw] in *) + (* let utilsT = TupleT [uT_r_aw (* 0 has_version *); uT_r_aw (* 1 id *)] in *) + (* let requestT = TupleT [cpT userT (* 0 user *); *) + (* cpT versionT (* 1 version *); *) + (* cpT utilsT (* 2 utils *); *) + (* cpT uT_r_aw (* 3 data *); *) + (* uT_r_aw (* 4 operation_date *)] in *) + (* let user_utilsE = TupleE [UnitE (* 0 id *); UnitE] in *) + (* let user_infoE = TupleE [UnitE (* 0 name *); UnitE; UnitE] in *) + (* let userE = TupleE [rfg0E (* 0 utils *); rfg1E (* 1 info *)] in *) + (* let versionE = TupleE [UnitE (* 0 id *); UnitE; UnitE] in *) + (* let utilsE = TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] in *) + (* let requestE = TupleE [rfg2E (* 0 user *); *) + (* rfg3E (* 1 version *); *) + (* rfg4E (* 2 utils *); *) + (* rfg5E (* 3 data *); *) + (* UnitE (* 4 operation_date *)] in *) + (* let get_version_idID = vg7 in *) + (* let updated_versionID = vg8 in *) + (* let sendID = vg9 in *) + (* let send_allID = vg10 in *) + (* let get_version_idF = FunD ([moded requestT], *) + (* (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in *) + (* let updated_versionF = FunD ([moded requestT], *) + (* (rdS @@ access 0 @@ drf @@ access 2 v0) #. *) (* TODO: read all the substructure ?? *) - (rdS @@ access 0 @@ drf @@ access 1 v0) #. - (rdS @@ access 1 @@ drf @@ access 1 v0)) in - let sendF = FunD ([moded requestT], - (( - (wrS @@ access 0 @@ drf @@ access 2 v0) #. - (rdS @@ drf @@ access 3 v0) #. - (wrS @@ drf @@ access 3 v0) #. - (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0) - ) |. skp) #. - (wrS @@ access 4 v0) #. + (* (rdS @@ 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]) #. + (* (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) #. + (* (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! |}] + (* ((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