simplest_model_with_mod: fixes & model spec fixes

simplest_model_with_mods/analyzer_cap.ml

@@ -95,8 +95,8 @@ struct
   let mem_add (state : state) (value : value) : state = match state with
     (env, mem, mem_len, visited) -> let mem = value :: mem in (env, mem, mem_len + 1, visited)
 
-  let mem_check (state : state) (id : data) : state =
+  let mem_check (state : state) (id : data) : unit =
-    if mem_get state id == BotV then raise @@ Incorrect_memory_access id else state
+    if mem_get state id == BotV then raise @@ Incorrect_memory_access id else ()
 
 
   let arg_to_value (state : state) (arg : arg) : value = match arg with
@@ -106,10 +106,10 @@ struct
   let st_mem_len (state : state) : int =
     match state with (_, _, mem_len, _) -> mem_len
 
-  (* TODO *)
   let check_tag_correct (tag : tag) (id : data) : unit =
     if (* (is_in tag && not (is_read tag)) || *) (* TODO: required ?? *)
-       is_out tag > is_write tag
+       is_out tag > is_write tag ||
+       is_read tag > is_in tag
        (* || is_copy tag && is_out tag *) (* ?? *)
     then raise @@ Invalid_argument_tag id
     else ()
@@ -131,25 +131,19 @@ struct
                       else let state_ext = env_add state id arg_tag mem_id in
                            mem_set state_ext id BotV
 
-  (* TODO: FIXME: do not spoil out arguments *)
+  (* TODO: use state_before ?? or state in some order (both orders ?, mod and then check ?) *)
-  (* TODO: FIXME: do write to tags that are out for args (code + semantics fix)
-    -> write to out args *)
   let st_spoil_by_args (state : state) (arg_tags : tag list) (args : data list) : state =
     match state with (env, mem, mem_len, _visited) ->
+    let state_before = state in
     let spoil_folder (state : state) (tag : tag) (id : data) : state =
       let parent_tag = fst (env_get state id) in
-      if not (is_copy tag) && not (is_out tag)
+      if is_write tag > is_write parent_tag then raise @@ Incorrect_const_cast id
-      then (if is_write tag > is_write parent_tag
+      else let state' = if is_read tag then (mem_check state_before id; state) else state (* NOTE: state override *)
-               (* || is_read tag > is_read parent_tag *) (* TODO FIXME: check that can read *)
+      in if not @@ is_write tag then state'
-            then raise @@ Incorrect_const_cast id
+      else match is_out tag with
-            else let state_checked = if is_read tag
+        | true -> mem_set state' id UnitV
-                                     then mem_check state id
+        | false -> if is_copy tag then state'
-                                     else state
+                   else mem_set state' id BotV
-                 in
-                 if is_write tag
-                 then mem_set state_checked id BotV
-                 else state_checked)
-      else state
     in List.fold_left2 spoil_folder state arg_tags args
 
   let list_drop n xs = List.of_seq @@ Seq.drop n @@ List.to_seq xs
@@ -382,7 +376,7 @@ struct
     [%expect {| done! |}]
 
   (* NOTE: changed semantics by comporasion with prev analyzer, new test *)
-  let%expect_test "function with ref two same ref args, read & write both & nothing" =
+  let%expect_test "function with ref two same ref args, read both & nothing" =
     eval_prog (
       [([ri_ref; ri_ref],[Read 0; Read 1; Read 1])],
       ([wi_value], [Write 0; Call (0, [0; 0]); ]));
@@ -390,21 +384,33 @@ struct
     [%expect {| done! |}]
 
   (* NOTE: changed semantics by comporasion with prev analyzer, new test *)
-  let%expect_test "function with ref & copy of the same arg, read both & nothing" =
+  let%expect_test "function with ref & copy of the same arg, read & write both & nothing" =
     eval_prog (
       [([rwi_ref; rwi_value],[Read 0; Read 1; Write 0; Write 1; Read 1])],
       ([wi_value], [Write 0; Call (0, [0; 0]); ]));
     Printf.printf "done!";
     [%expect {| done! |}]
 
+  (* NOTE: changed semantics by comporasion with prev analyzer, new test *)
+  let%expect_test "function with copy & ref of the same arg, read & write both & nothing" =
+    eval_prog (
+      [([rwi_value; rwi_ref],[Read 0; Read 1; Write 0; Write 1; Read 1])],
+      ([wi_value], [Write 0; Call (0, [0; 0]); ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  (* TODO: FIXME: now correct (use state before for mem check), is this good ?, proper way to fix ? *)
   (* NOTE: maybe important case in the future *)
   let%expect_test "function with ref two same ref args, read & write both, error" =
-    try (eval_prog (
+    (* try ( *)
+      eval_prog (
       [([rwi_ref; rwi_ref],[Read 0; Read 1; Write 0; Write 1; Read 1])],
       ([wi_value], [Write 0; Call (0, [0; 0]); ]));
-         [%expect.unreachable])
+         (* [%expect.unreachable]) *)
-    with Incorrect_memory_access id -> Printf.printf "%i" id;
+    (* with Incorrect_memory_access id -> Printf.printf "%i" id; *)
-    [%expect {| 0 |}]
+    (* [%expect {| 0 |}] *)
+    Printf.printf "done!";
+    [%expect {| done! |}]
 
   (* >> tests with several functions *)
 
@@ -468,4 +474,8 @@ struct
     eval_prog ([([rwi_value], [Write 0; Read 0; Write 0; Call (0, [0])])], ([wi_value], [Write 0; Call (0, [0]) ]));
     Printf.printf "done!";
     [%expect {| done! |}]
+
+  (* --- *)
+
+  (* TODO: out arguments test, etc. *)
 end

simplest_model_with_mods/model.typ

@@ -29,19 +29,19 @@
 #let prog = `prog`
 #bnf(
   Prod(`read`,
-    { Or[Read][]
+    { Or[Read][read passed value]
       Or[Not Read][] } ),
   Prod(`write`,
-    { Or[Write][]
+    { Or[Write][write to passed variable]
       Or[Not Write][] } ),
   Prod(`copy`,
-    { Or[Ref][]
+    { Or[Ref][pass reference to the value]
-      Or[Value][] } ),
+      Or[Value][pass copy of te value] } ),
   Prod(`in`,
-    { Or[In][]
+    { Or[In][parameter value used as input]
       Or[Not In][] } ),
   Prod(`out`,
-    { Or[Out][]
+    { Or[Out][parametr value returned]
       Or[Not Out][] } ),
   Prod(
     `tag`,
@@ -88,8 +88,6 @@
 )
 == Семантика статического интерпретатора
 
-*TODO: исправить с обычного интерпретатора*
-
 #h(10pt)
 
 $V := value$ - значения памяти
@@ -100,8 +98,6 @@ $X$ - можество переменных
 
 *TODO: специфицировать доступ*
 
-*TODO: формально описать isCorrect для tag-а*
-
 *TODO: формально описать accessor-ы tag*
 
 $sigma : X -> tag times L$ - #[ позиции памяти, соответстующие переменным контекста,