diff --git a/model_with_structures/analyzer_rw.ml b/model_with_structures/analyzer_rw.ml index fdf70d5..a437d81 100644 --- a/model_with_structures/analyzer_rw.ml +++ b/model_with_structures/analyzer_rw.ml @@ -191,8 +191,10 @@ struct let rec valbuild (mem : mem) (t : atype) : mem * value = match t with + | UnitT (Rd, _) -> (mem, UnitV (ZeroMV, ZeroRV, ZeroWV)) + | UnitT (NRd, _) -> (mem, UnitV (BotMV, ZeroRV, ZeroWV)) (* NOTE: ignore pre-tag in rw-analysis *) - | UnitT (_, _) -> (mem, UnitV (ZeroMV, ZeroRV, ZeroWV)) + | UnitT (UndefRd, _) -> (mem, UnitV (ZeroMV, ZeroRV, ZeroWV)) | FunT _ -> raise @@ Typing_error "valbuild: funciton value is not supported" | RefT (_, t) -> let (mem', v') = valbuild mem t in let (mem'', id'') = mem_add mem' v' in @@ -323,12 +325,6 @@ struct (* TODO: better way ??? *) let globals_min_id : data = 1000 - let prog_init (prog : prog) : state = - match prog with (decls, _) -> fst @@ List.fold_left (* TODO: FIXME: check x's order *) - (fun (st, x) d -> (add_decl st x d, x + 1)) - (empty_state, globals_min_id) - decls - (* - call values spoil *) (* TODO: check assignment type matches types separately later ?? *) @@ -441,17 +437,20 @@ struct | SmthWV -> MayWr | OneWV -> AlwaysWr - let rec tags_check (mem : mem) (v : value) (t : atype) : unit = + (* NOTE: in analyzer rw tags check replaces tags with calculated ones *) + let rec tags_check (mem : mem) (v : value) (t : atype) : atype = match v, t with | UnitV (v_m, v_r, v_w), UnitT (r, w) -> - if readval_to_cap v_r != r - then raise @@ Eval_error "tags_check: wrong 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 + let r' = readval_to_cap v_r in + let w' = writeval_to_cap v_w in + if r != UndefRd && r != r' + then raise @@ Eval_error "tags_check: not undef read tag & not correct" + else if w != UndefWr && w != w' + then raise @@ Eval_error "tags_check: not undef write tag & not correct" + else UnitT (r', w') + | FunV, FunT _ -> t + | RefV id, RefT (c, t) -> RefT (c, tags_check mem (mem_get mem id) t) + | TupleV vs, TupleT ts -> TupleT (List.map2 (tags_check mem) vs ts) | _, _ -> raise @@ Typing_error "tags_check" (* - writability check *) @@ -510,28 +509,42 @@ struct (* - function evaluation *) - let rec func_eval (state : state) (d : decl) : unit = + (* NOTE: in analyzer rw replaces read & write tags with calculated ones *) + let rec func_eval (state : state) (d : decl) : decl = match d with | FunD (ts, stmt) -> (let (state_with_args, _) = List.fold_left (fun (st, x) (m, t) -> (addarg st x t, x + 1)) (state, 0) ts in match stmt_eval state_with_args stmt with (mem_after_stmt, _, vals_after_stmt) -> - ignore @@ List.fold_left - (fun x (_, t) -> + let (_, ts') = List.fold_left + (fun (x, ts_acc) (m, 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) - | VarD _ -> () + let t' = tags_check mem_after_stmt v t in + (x + 1, (m, t') :: ts_acc)) + (0, []) ts in + (* TODO: FIXME: isure that need reverse ? *) + FunD (List.rev ts', stmt)) + | VarD _ -> d (* --- program execution --- *) - let prog_eval (prog : prog) : state = + (* NOTE: decls returned in the reversed order (?) *) + let prog_init (prog : prog) : (state * decl list) = + match prog with (decls, _) -> let (st', decls', _) = List.fold_left (* TODO: FIXME: check x's order *) + (fun (st, decls', x) d -> + let d' = func_eval st d in + (add_decl st x d', d' :: decls', x + 1)) + (empty_state, [], globals_min_id) + decls in + (st', List.rev decls') + + let prog_eval (prog : prog) : prog = match prog with (decls, s) -> - let init_state = prog_init prog in - ignore @@ List.map (func_eval init_state) decls; - stmt_eval init_state s + let (init_state, decls') = prog_init prog in + ignore @@ stmt_eval init_state s; + (decls', s) let prog_eval_noret (prog : prog) : unit = ignore @@ prog_eval prog @@ -837,23 +850,23 @@ struct Printf.printf "done!"; [%expect {| done! |}] - (* NOTE: memoization used *) - let%expect_test "call inside call, recursive, dsl" = - prog_eval_noret ( - [ - defg uT_r_aw; - defg (rfT uT_r_aw); - FunD ( - [moded @@ cpT @@ uT_aw], - (callS vg2 [pE v0]) #. - (wrS @@ drf @@ v0) - ) - ], - (callS vg2 [pE vg1]) #. - (rdS @@ drf @@ vg1) - ); - Printf.printf "done!"; - [%expect {| done! |}] + (* NOTE: does not work for annalyzer rw to the sequenced declaration addition to calculate tags *) + (* let%expect_test "call inside call, recursive, dsl" = *) + (* prog_eval_noret ( *) + (* [ *) + (* defg uT_r_aw; *) + (* defg (rfT uT_r_aw); *) + (* FunD ( *) + (* [moded @@ cpT @@ uT_aw], *) + (* (callS vg2 [pE v0]) #. *) + (* (wrS @@ drf @@ v0) *) + (* ) *) + (* ], *) + (* (callS vg2 [pE vg1]) #. *) + (* (rdS @@ drf @@ vg1) *) + (* ); *) + (* Printf.printf "done!"; *) + (* [%expect {| done! |}] *) let%expect_test "call to fix after call, dsl" = prog_eval_noret (