controw flow: synthesizer write modes addition (no tests fix for always and may inersection)

model_with_control_flow/analyzer.ml

@@ -6,7 +6,7 @@ struct
   type data = int
 
   type read_cap = Rd | NRd
-  type write_cap = Wr | NWr
+  type write_cap = AlwaysWr | MayWr | NeverWr
   type copy_cap = Cp | NCp
 
   type in_cap = In | NIn
@@ -14,7 +14,7 @@ struct
 
   type tag = read_cap * write_cap * copy_cap * in_cap * out_cap
 
-  type stmt = Call of data * data list | Read of data | Write of data
+  type stmt = Call of data * data list | Read of data | Write of data | Choice of stmt list * stmt list
 
   type body = stmt list
 
@@ -29,12 +29,13 @@ struct
   exception Ref_rvalue_argument of int
   exception Incorrect_const_cast of int
   exception Invalid_argument_tag of int
+  exception Incompatible_states
 
   (* --- static interpreter (no rec) --- *)
 
   (* TODO: allow data (rvalue) in calls ?? *)
   type arg = RValue | LValue of data
-  type value = UnitV | BotV (* NOTE: RefV of data - not needed for now *)
+  type value = UnitV | UndefV | BotV (* NOTE: RefV of data - not needed for now *)
 
   type env = (int * (tag * data)) list
 
@@ -43,25 +44,55 @@ struct
 
   (* --- *)
 
+  let rec list_zip_with f xs ys = match xs, ys with (* TODO: alternative from stdlib *)
+    | x :: xs, y :: ys -> f x y :: list_zip_with f xs ys 
+    | _, _ -> []
+
+  (* --- *)
+
+  let value_combine (left : value) (right : value) : value = match left, right with
+    | UnitV, UnitV -> UnitV
+    | BotV, BotV -> BotV
+    | _, _ -> UndefV (* NOTE: should be expanded in relational interpreter to not use ineq (?) *)
+
+  let memory_combine (left : value list) (right : value list) : value list =
+    list_zip_with value_combine left right
+
+  let state_combine (left : state) (right : state) : state = match left, right with
+    (lenv, lmem, lmem_len, lvisited), (renv, rmem, rmem_len, rvisited) ->
+    if lenv != renv || lmem_len != rmem_len || lvisited != rvisited then raise Incompatible_states
+    else (lenv, memory_combine lmem rmem, lmem_len, List.append lvisited rvisited) (* TODO: union visited lists instead ? *)
+
+  (* --- *)
+
   let is_read (tag : tag) : bool = match tag with
     | (Rd, _, _, _, _) -> true
-    | (NRd, _, _, _, _) -> false
+    | _ -> false
 
-  let is_write (tag : tag) : bool = match tag with
+  let is_always_write (tag : tag) : bool = match tag with
-    | (_, Wr, _, _, _) -> true
+    | (_, AlwaysWr, _, _, _) -> true
-    | (_, NWr, _, _, _) -> false
+    | _ -> false
+
+  let is_may_write (tag : tag) : bool = match tag with
+    | (_, AlwaysWr, _, _, _) -> true
+    | (_, MayWr, _, _, _) -> true
+    | _ -> false
+
+  let is_never_write (tag : tag) : bool = match tag with
+    | (_, NeverWr, _, _, _) -> true
+    | _ -> false
 
   let is_copy (tag : tag) : bool = match tag with
     | (_, _, Cp, _, _) -> true
-    | (_, _, NCp, _, _) -> false
+    | _ -> false
 
   let is_in (tag : tag) : bool = match tag with
     | (_, _, _, In, _) -> true
-    | (_, _, _, NIn, _) -> false
+    | _ -> false
 
   let is_out (tag : tag) : bool = match tag with
     | (_, _, _, _, Out) -> true
-    | (_, _, _, _, NOut) -> false
+    | _ -> false
 
   (* --- *)
 
@@ -108,7 +139,7 @@ struct
 
   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_always_write tag ||
        is_read tag > is_in tag
        (* || is_copy tag && is_out tag *) (* ?? *)
     then raise @@ Invalid_argument_tag id
@@ -123,7 +154,7 @@ struct
     else match arg with
       | RValue -> raise @@ Ref_rvalue_argument id (* TODO: allow later ?? *)
       | LValue arg -> let (parent_tag, mem_id) = env_get state_before arg in
-                      if is_write arg_tag > is_write parent_tag
+                      if is_may_write arg_tag > is_always_write parent_tag (* TODO: FIXME: not updated semantics ?? *)
                       then raise @@ Incorrect_const_cast id
                       else if is_read arg_tag
                       then env_add state id arg_tag mem_id
@@ -141,12 +172,12 @@ struct
       (* NOTE: replaced with later condition *)
       (* if is_write tag > is_write parent_tag && (not (is_copy tag) || is_out tag) then raise @@ Incorrect_const_cast idi else *)
       let state = if is_read tag then (mem_check state_before id; state) else state (* NOTE: state override *)
-      in if not @@ is_write tag then state
+      in if is_never_write tag then state (* TODO: FIXME: check *)
       else match is_out tag with
-        | true -> if not @@ is_write parent_tag then raise @@ Incorrect_const_cast id
+        | true -> if not @@ is_always_write parent_tag then raise @@ Incorrect_const_cast id
                   else mem_set state id UnitV
         | false -> if is_copy tag then state
-                   else if not @@ is_write parent_tag then raise @@ Incorrect_const_cast id
+                   else if not @@ is_may_write parent_tag then raise @@ Incorrect_const_cast id (* TODO: check that may modifier correct *)
                    else mem_set state id BotV
     in List.fold_left2 spoil_folder state arg_tags args
 
@@ -163,9 +194,13 @@ struct
                                                state_fun
                              in st_spoil_by_args state_with_visited arg_tags args
       | Read id -> mem_check state id; state
-      | Write id -> if is_write @@ fst @@ env_get state id
+      | Write id -> if is_may_write @@ fst @@ env_get state id
                     then mem_set state id UnitV
                     else raise @@ Incorrect_const_cast id
+      | Choice (xs, ys) -> let state_x = eval_body state prog xs in
+                           let state_y = eval_body state prog ys in
+                           state_combine state_x state_y
+                           (* TODO: FIXME: additional may write / always write checks ?? *)
 
   and eval_body (state : state) (prog : fun_decl list) (body : body) : state =
     List.fold_left (fun state stmt -> eval_stmt state prog stmt) state body
@@ -192,14 +227,18 @@ struct
 
   (* tests *)
 
-  let rwi_value : tag = (Rd, Wr, Cp, In, NOut)
+  let rwi_value : tag = (Rd, AlwaysWr, Cp, In, NOut)
-  let ri_value : tag = (Rd, NWr, Cp, In, NOut)
+  let rmwi_value : tag = (Rd, MayWr, Cp, In, NOut)
-  let wi_value : tag = (NRd, Wr, Cp, In, NOut)
+  let ri_value : tag = (Rd, NeverWr, Cp, In, NOut)
-  let i_value : tag = (NRd, NWr, Cp, In, NOut)
+  let wi_value : tag = (NRd, AlwaysWr, Cp, In, NOut)
-  let rwi_ref : tag = (Rd, Wr, NCp, In, NOut)
+  let mwi_value : tag = (NRd, MayWr, Cp, In, NOut)
-  let ri_ref : tag = (Rd, NWr, NCp, In, NOut)
+  let i_value : tag = (NRd, NeverWr, Cp, In, NOut)
-  let wi_ref : tag = (NRd, Wr, NCp, In, NOut)
+  let rwi_ref : tag = (Rd, AlwaysWr, NCp, In, NOut)
-  let i_ref : tag = (NRd, NWr, NCp, In, NOut)
+  let rmwi_ref : tag = (Rd, MayWr, NCp, In, NOut)
+  let ri_ref : tag = (Rd, NeverWr, NCp, In, NOut)
+  let wi_ref : tag = (NRd, AlwaysWr, NCp, In, NOut)
+  let mwi_ref : tag = (NRd, MayWr, NCp, In, NOut)
+  let i_ref : tag = (NRd, NeverWr, NCp, In, NOut)
 
   (* >> tests without functions *)
 
@@ -475,4 +514,9 @@ struct
   (* --- *)
 
   (* TODO: out arguments test, etc. *)
+
+  (* --- *)
+
+  (* TODO: combine statement tests *)
+
 end

model_with_control_flow/dune

@@ -17,7 +17,7 @@
  (name tests_cf)
  (modules tests)
  (flags (-rectypes))
- (libraries synthesizer_mods tests_f_mods)
+ (libraries synthesizer_cf tests_f_cf)
  (inline_tests)
  (wrapped false)
  (preprocess
@@ -27,7 +27,7 @@
  (name tests_f_cf)
  (modules tests_f)
  (flags (-rectypes))
- (libraries OCanren OCanren.tester synthesizer_mods)
+ (libraries OCanren OCanren.tester synthesizer_cf)
  (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
  (wrapped false)
  (preprocess

model_with_control_flow/synthesizer.ml

@@ -22,7 +22,7 @@ struct
   module WriteCap = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec t = Wr | NWr
+      type nonrec t = AlwaysWr | MayWr | NeverWr
       [@@deriving gt ~options:{ show; gmap }]
       type nonrec ground = t
     ]
@@ -72,49 +72,49 @@ struct
                   let open CopyCap in
                   let open InCap in
                   let open OutCap in
-                  ocanren { Tag (Rd, Wr, Val, In, NOut) }
+                  ocanren { Tag (Rd, AlwaysWr, Val, In, NOut) }
     let ri_val = let open ReadCap in
                  let open WriteCap in
                  let open CopyCap in
                  let open InCap in
                  let open OutCap in
-                 ocanren { Tag (Rd, NWr, Val, In, NOut) }
+                 ocanren { Tag (Rd, NeverWr, Val, In, NOut) }
     let wi_val = let open ReadCap in
                  let open WriteCap in
                  let open CopyCap in
                  let open InCap in
                  let open OutCap in
-                 ocanren { Tag (NRd, Wr, Val, In, NOut) }
+                 ocanren { Tag (NRd, AlwaysWr, Val, In, NOut) }
     let i_val = let open ReadCap in
                 let open WriteCap in
                 let open CopyCap in
                 let open InCap in
                 let open OutCap in
-                ocanren { Tag (NRd, NWr, Val, In, NOut) }
+                ocanren { Tag (NRd, NeverWr, Val, In, NOut) }
     let rwi_ref = let open ReadCap in
                   let open WriteCap in
                   let open CopyCap in
                   let open InCap in
                   let open OutCap in
-                  ocanren { Tag (Rd, Wr, Ref, In, NOut) }
+                  ocanren { Tag (Rd, AlwaysWr, Ref, In, NOut) }
     let ri_ref = let open ReadCap in
                  let open WriteCap in
                  let open CopyCap in
                  let open InCap in
                  let open OutCap in
-                 ocanren { Tag (Rd, NWr, Ref, In, NOut) }
+                 ocanren { Tag (Rd, NeverWr, Ref, In, NOut) }
     let wi_ref = let open ReadCap in
                  let open WriteCap in
                  let open CopyCap in
                  let open InCap in
                  let open OutCap in
-                 ocanren { Tag (NRd, Wr, Ref, In, NOut) }
+                 ocanren { Tag (NRd, AlwaysWr, Ref, In, NOut) }
     let i_ref = let open ReadCap in
                 let open WriteCap in
                 let open CopyCap in
                 let open InCap in
                 let open OutCap in
-                ocanren { Tag (NRd, NWr, Ref, In, NOut) }
+                ocanren { Tag (NRd, NeverWr, Ref, In, NOut) }
 
     (* constraints *)
     let x_any tag = let open InCap in
@@ -141,12 +141,16 @@ struct
     let is_not_reado tag = let open ReadCap in ocanren {
                              fresh w_, c_, i_, o_ in
                              tag == Tag (NRd, w_, c_, i_, o_) }
-    let is_writeo tag = let open WriteCap in ocanren {
+    let is_always_writeo tag = let open WriteCap in ocanren {
-                          fresh r_, c_, i_, o_ in
+                                 fresh r_, c_, i_, o_ in
-                          tag == Tag (r_, Wr, c_, i_, o_) }
+                                 tag == Tag (r_, AlwaysWr, c_, i_, o_) }
-    let is_not_writeo tag = let open WriteCap in ocanren {
+    let is_may_writeo tag = let open WriteCap in ocanren {
                               fresh r_, c_, i_, o_ in
-                              tag == Tag (r_, NWr, c_, i_, o_) }
+                              { tag == Tag (r_, AlwaysWr, c_, i_, o_) |
+                                tag == Tag (r_, MayWr, c_, i_, o_) } }
+    let is_never_writeo tag = let open WriteCap in ocanren {
+                                fresh r_, c_, i_, o_ in
+                                tag == Tag (r_, NeverWr, c_, i_, o_) }
     let is_refo tag = let open CopyCap in ocanren {
                         fresh r_, w_, i_, o_ in
                         tag == Tag (r_, w_, Ref, i_, o_) }
@@ -178,7 +182,7 @@ struct
                                                               let open CopyCap in
                                                               let open InCap in
                                                               let open OutCap in
-                                                              ocanren {q == Tag (Rd, NWr, Ref, In, NOut)})
+                                                              ocanren {q == Tag (Rd, NeverWr, Ref, In, NOut)})
                                                     (fun q -> q#reify reify)))
     end
   end
@@ -438,7 +442,7 @@ struct
   let tag_correcto tg =
     let open Tag in
     ocanren {
-      {is_not_outo tg | { is_outo tg & is_writeo tg } } &
+      {is_not_outo tg | { is_outo tg & is_always_writeo tg } } &
       {is_not_reado tg | { is_reado tg & is_ino tg } }
     }
 
@@ -461,7 +465,7 @@ struct
           arg == LValue arg' &
           env_geto state_before id parent_tag mem_id &
           env_addo state id arg_tag mem_id state' &
-          { is_not_writeo arg_tag | { is_writeo arg_tag & is_writeo parent_tag } } &
+          { is_never_writeo arg_tag | { is_may_writeo arg_tag & is_may_writeo parent_tag } } &
           {
             { is_reado arg_tag & state' == state'' } |
             { is_not_reado arg_tag & mem_seto state' id Bot state'' }
@@ -478,14 +482,13 @@ struct
       fresh env, mem, mem_len, _visited, parent_tg, _mem_id in
       state == St (env, mem, mem_len, _visited) &
       env_geto state id parent_tg _mem_id &
-      (* NOTE: replaced with later condition (this one needs fix) *)
-      (* { is_not_writeo tg | { is_writeo tg & is_writeo parent_tg } } & *)
       { is_not_reado tg | { is_reado tg & mem_checko state_before id } } &
-      { { is_not_writeo tg & state == state'} |
+      { { is_never_writeo tg & state == state'} |
-        { is_writeo tg & {
+        { is_always_writeo tg & 
-          { is_outo tg & is_writeo parent_tg & mem_seto state id Unit state' } |
+          is_outo tg & is_may_writeo parent_tg & mem_seto state id Unit state' } |
+        { is_may_writeo tg & {
           { is_not_outo tg & is_valueo tg & state == state' } |
-          { is_not_outo tg & is_refo tg & is_writeo parent_tg & mem_seto state id Bot state' }
+          { is_not_outo tg & is_refo tg & is_may_writeo parent_tg & mem_seto state id Bot state' }
         } }
       }
     }
@@ -578,7 +581,7 @@ struct
     { fresh id, tag, _mem_id in
       stmt == Write id &
       env_geto state id tag _mem_id &
-      is_writeo tag &
+      is_may_writeo tag &
       mem_seto state id Unit state' }
   }
 

model_with_control_flow/tests.ml

@@ -3,14 +3,14 @@ open Synthesizer
 open Relational
 
 (* type tests *)
-let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NWr, Ref, In, NOut)] |}]
+let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}]
 let%expect_test "Stmt type test (1)" = print_endline (Stmt.Test.test1 ()); [%expect {| [[S (S (O))]] |}]
 let%expect_test "Stmt type test (2)" = print_endline (Stmt.Test.test2 ()); [%expect {| [Call (S (O), [S (S (O))])] |}]
-let%expect_test "FunDecl type test" = print_endline (FunDecl.Test.test ()); [%expect {| [FunDecl ([Tag (Rd, Wr, Ref, In, NOut); Tag (Rd, Wr, Val, In, NOut)], [Call (S (O), [O]); Write (S (O))])] |}]
+let%expect_test "FunDecl type test" = print_endline (FunDecl.Test.test ()); [%expect {| [FunDecl ([Tag (Rd, AlwaysWr, Ref, In, NOut); Tag (Rd, AlwaysWr, Val, In, NOut)], [Call (S (O), [O]); Write (S (O))])] |}]
-let%expect_test "Prog type test" = print_endline (Prog.Test.test ()); [%expect {| [Prog ([], FunDecl ([Tag (Rd, NWr, Val, In, NOut)], [Write (O); Read (O)]))] |}]
+let%expect_test "Prog type test" = print_endline (Prog.Test.test ()); [%expect {| [Prog ([], FunDecl ([Tag (Rd, NeverWr, Val, In, NOut)], [Write (O); Read (O)]))] |}]
 let%expect_test "Arg type test" = print_endline (Arg.Test.test ()); [%expect {| [LValue (S (S (S (O))))] |}]
 let%expect_test "Value type test" = print_endline (Value.Test.test ()); [%expect {| [Bot; Unit] |}]
-let%expect_test "St type test" = print_endline (St.Test.test ()); [%expect {| [St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Bot], S (O), [O])] |}]
+let%expect_test "St type test" = print_endline (St.Test.test ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Bot], S (O), [O])] |}]
 
 (* function tests *)
 let%expect_test "inv_id test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}]
@@ -19,20 +19,20 @@ let%expect_test "inv_id test 3" = print_endline (inv_id_t3 ()); [%expect {| [S (
 let%expect_test "list_drop test" = print_endline (list_drop_t ()); [%expect {| [[S (S (S (O)))]] |}]
 let%expect_test "list_replace test" = print_endline (list_replace_t ()); [%expect {| [[S (O); O; S (S (S (O))); S (S (S (S (O))))]] |}]
 let%expect_test "arG_to_value test 1" = print_endline (arg_to_value_t ()); [%expect {| [Unit] |}]
-let%expect_test "st_add_arg test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
+let%expect_test "st_add_arg test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
-let%expect_test "write eval test 1" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [])] |}]
+let%expect_test "write eval test 1" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [])] |}]
-let%expect_test "write eval test 2" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [])] |}]
+let%expect_test "write eval test 2" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [])] |}]
-let%expect_test "multiple writes eval test" = print_endline (writes_eval_t ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit; Unit], S (S (O)), [])] |}]
+let%expect_test "multiple writes eval test" = print_endline (writes_eval_t ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Unit], S (S (O)), [])] |}]
-let%expect_test "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot], S (O), [O])] |}]
+let%expect_test "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [O])] |}]
-let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [O])] |}]
+let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [O])] |}]
-let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [O])] |}]
+let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [O])] |}]
-let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}]
+let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}]
-let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}]
+let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}]
-let%expect_test "mem_set test 1" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit], S (O), [])] |}]
+let%expect_test "mem_set test 1" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit], S (O), [])] |}]
-let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot], S (O), [])] |}]
+let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [])] |}]
-let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), S (O)))], [Bot; Unit], S (S (O)), [])] |}]
+let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O)))], [Bot; Unit], S (S (O)), [])] |}]
-let%expect_test "add_arg_folder test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
+let%expect_test "add_arg_folder test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
-let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
+let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
 let%expect_test "rvalue test" = print_endline (rvalue_t ()); [%expect {| [[]; [RValue]; [RValue; RValue]] |}]
 let%expect_test "empty_state test" = print_endline (empty_state_t ()); [%expect {| [St ([], [], O, [])] |}]
 let%expect_test "function eval test 1" = print_endline (fun_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}]
@@ -47,10 +47,10 @@ let%expect_test "prog eval test 3" = print_endline (prog_eval_t3 ()); [%expect {
 let%expect_test "prog eval test 4" = print_endline (prog_eval_t4 ()); [%expect {| [] |}]
 let%expect_test "prog eval test 5" = print_endline (prog_eval_t5 ()); [%expect {| [St ([], [], O, [O])] |}]
 let%expect_test "prog eval test 6" = print_endline (prog_eval_t6 ()); [%expect {| [] |}]
-let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Tag (Rd, Wr, Val, In, NOut); Tag (NRd, Wr, Val, In, NOut)] |}]
+let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Tag (Rd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)] |}]
-let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Tag (NRd, Wr, Val, In, NOut); Tag (NRd, Wr, Ref, In, NOut)] |}]
+let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Ref, In, NOut)] |}]
-let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Tag (NRd, Wr, Val, In, NOut); Tag (NRd, Wr, Val, In, NOut)]; [Tag (NRd, Wr, Ref, In, NOut); Tag (NRd, Wr, Val, In, NOut)]] |}]
+let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]; [Tag (NRd, AlwaysWr, Ref, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]] |}]
-let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Tag (NRd, Wr, Val, In, NOut)]] |}]
+let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut)]] |}]
 let%expect_test "synthesis test 5" = print_endline (synt_t5 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Val]; [Ref; Ref]] |}]
 let%expect_test "synthesis test 6" = print_endline (synt_t6 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Ref]; [Ref; Val]] |}]
 let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[Val; Val]; [Ref; Val]] |}]

model_with_control_flow/tests_f.ml

@@ -432,7 +432,7 @@ let synt_t5 _ = show(answerCopyCaps) (Stream.take (run qr
             let open St in
             ocanren {fresh q', r' in
                      i_any q' & is_not_reado q' &
-                     i_any r' & is_not_reado r' & is_not_writeo r' &
+                     i_any r' & is_not_reado r' & is_never_writeo r' &
                      eq_copyo q' q & eq_copyo r' r &
                      eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])],
                                        FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
@@ -447,7 +447,7 @@ let synt_t6 _ = show(answerCopyCaps) (Stream.take (run qr
             let open St in
             ocanren {fresh q', r' in
                      i_any q' & is_not_reado q' &
-                     i_any r' & is_not_reado r' & is_not_writeo r' &
+                     i_any r' & is_not_reado r' & is_never_writeo r' &
                      eq_copyo q' q & eq_copyo r' r &
                      eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])],
                                        FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
@@ -490,7 +490,7 @@ let synt_t9 _ = show(answerCopyCaps) (Stream.take (run qr
             let open St in
             ocanren {fresh q', r' in
                      i_any q' & is_not_reado q' &
-                     i_any r' & is_reado r' & is_not_writeo r' &
+                     i_any r' & is_reado r' & is_never_writeo r' &
                      eq_copyo q' q & eq_copyo r' r &
                      eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Read 1])],
                                        FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, [0]))})