struct: some synt. tests (some test bodies without actual check)

model_with_structures/analyzer.ml

@@ -290,7 +290,7 @@ struct
     (r != Rd || v == ZeroV) &&
     (r != Rd || fst m == In) &&
     (snd m != Out || w == AlwaysWr) &&
-    (* TODO: check *)
+    (* TODO: FIXME: check *)
     ((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr) &&
     is_trivial_v v
 
@@ -570,7 +570,7 @@ struct
 
   (* let%expect_test "simple call with write" = *)
     (* prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE); *)
-                      (* VarD (RefT (Rf, (UnitT (Rd, MayWr))), RefE globals_min_id); *)
+                      (* VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE globals_min_id); *)
                       (* FunD ([((In, NOut), RefT (Cp, UnitT (Rd, MayWr)))], WriteS (DerefP (VarP 0)))], *)
                      (* CallS (VarP (globals_min_id + 2), *)
                             (* [PathE (VarP (globals_min_id + 1))])); *)

model_with_structures/synthesizer.ml

@@ -482,14 +482,11 @@ struct
         v == RefV id &
         tp == RefT (c, tp') &
         { { c == Rf & mem_with_id' == Std.pair mem v } |
-          { fresh v, mem_cp, v_cp, mem_with_v_cp,
+          { fresh v', mem_cp, v_cp, mem_add, id_add in
-                  mem_add, id_add, mem_with_id_add in
             c == Cp &
-            mem_geto mem id v &
+            mem_geto mem id v' &
-            valcopyo mem v tp mem_with_v_cp &
+            valcopyo mem v' tp' (Std.pair mem_cp v_cp) &
-            Std.pair mem v_cp == mem_with_v_cp &
+            mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
-            mem_addo mem_cp v_cp mem_with_id_add &
-            Std.pair mem_add id_add == mem_with_id_add &
             mem_with_id' == (mem_add, RefV id_add) } } } |
       { fresh vs, tps, init_mem_with_vs, mem_with_vs', mem', vs' in
         v == TupleV vs &
@@ -881,7 +878,9 @@ struct
           (* TODO: FIXME check left or right order *)
           list_foldl2o (stmt_eval_spoil_foldero types vals)
                       mem tps es mem_spoiled &
-          st' == StEnv (mem_spoiled, types, vals) } |
+          (* st' == state_with_args *)
+          st' == StEnv (mem_spoiled, types, vals)
+        } |
         { fresh p, tp, _r, w, x, id, v,
                 mem_upd, v_upd, mem_set in
           s == WriteS p &

model_with_structures/tests.ml

@@ -24,6 +24,24 @@ let%expect_test "simple var, write & read" = print_endline(prog_eval_t_simple_va
 let%expect_test "simple call with read" = print_endline(prog_eval_t_simple_call_rd ());
   [%expect {| [StEnv (MemEnv ([FunV ([ReadS (VarP (O))]); ZeroV], S (S (O))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), UnitT (Rd, NeverWr))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, NeverWr))], [(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), UnitT (Rd, NeverWr))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, NeverWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}]
 
+let%expect_test "simple call with ref read" = print_endline(prog_eval_t_simple_call_rd_ref ());
+  [%expect {| [StEnv (MemEnv ([FunV ([ReadS (DerefP (VarP (O)))]); RefV (O); ZeroV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}]
+
+let%expect_test "simple call with write" = print_endline(prog_eval_t_simple_call_wr ());
+  [%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); ZeroV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}]
+
+let%expect_test "simple call with read after write" = print_endline(prog_eval_t_simple_call_wr_rd ());
+  [%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (DerefP (VarP (O))), ReadS (DerefP (VarP (O))))]); RefV (O); BotV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}]
+
+let%expect_test "simple call with forbidden write" = print_endline(prog_eval_t_simple_call_fbd_wr ());
+  [%expect {| [] |}]
+
+let%expect_test "simple call with write to ref" = print_endline(prog_eval_t_simple_call_ref_wr ());
+  [%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); BotV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}]
+
+let%expect_test "simple call with forbidden write to ref" = print_endline(prog_eval_t_simple_call_ref_fbd_wr ());
+  [%expect {| [] |}]
+
 (* type tests *)
 (* 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))]] |}] *)

model_with_structures/tests_f.ml

@@ -10,6 +10,7 @@ open Decl
 open Type
 open Expr
 open Path
+open CopyCap
 open ReadCap
 open WriteCap
 open InCap
@@ -109,10 +110,189 @@ let prog_eval_t_simple_call_rd _ = show(answer) (Stream.take (run q
               xd == VarD (UnitT (Rd, NeverWr), UnitE) &
               fd == FunD ([(Mode (In, NOut), UnitT (Rd, NeverWr))], ReadS (VarP 0)) &
               prog == Prg ([xd; fd], CallS (VarP fg, [PathE (VarP xg)])) &
+              prog_evalo prog q })
+  (fun q -> q#reify (StEnv.prj_exn))))
+
+let prog_eval_t_simple_call_rd_ref _ = show(answer) (Stream.take (run q
+  (fun q -> ocanren {
+              fresh prog, xg, yg, fg, xd, yd, fd, st in
+              globals_min_ido xg &
+              yg == Nat.s xg &
+              fg == Nat.s yg &
+              xd == VarD (UnitT (Rd, MayWr), UnitE) &
+              yd == VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE xg) &
+              fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))],
+                          ReadS (DerefP (VarP 0))) &
+              prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
+              prog_evalo prog q })
+  (fun q -> q#reify (StEnv.prj_exn))))
+
+let prog_eval_t_simple_call_wr _ = show(answer) (Stream.take (run q
+  (fun q -> ocanren {
+              fresh prog, xg, yg, fg, xd, yd, fd, st in
+              globals_min_ido xg &
+              yg == Nat.s xg &
+              fg == Nat.s yg &
+              xd == VarD (UnitT (Rd, MayWr), UnitE) &
+              yd == VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE xg) &
+              fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))],
+                          WriteS (DerefP (VarP 0))) &
+              prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
+              prog_evalo prog q })
+  (fun q -> q#reify (StEnv.prj_exn))))
+
+let prog_eval_t_simple_call_wr_rd _ = show(answer) (Stream.take (run q
+  (fun q -> ocanren {
+              fresh prog, xg, yg, fg, xd, yd, fd, st in
+              globals_min_ido xg &
+              yg == Nat.s xg &
+              fg == Nat.s yg &
+              xd == VarD (UnitT (NRd, MayWr), UnitE) &
+              yd == VarD (RefT (Rf, UnitT (NRd, MayWr)), RefE xg) &
+              fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
+                          SeqS (WriteS (DerefP (VarP 0)),
+                                ReadS (DerefP (VarP 0)))) &
+              prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
+              prog_evalo prog q })
+  (fun q -> q#reify (StEnv.prj_exn))))
+
+let prog_eval_t_simple_call_fbd_wr _ = show(answer) (Stream.take (run q
+  (fun q -> ocanren {
+              fresh prog, xg, yg, fg, xd, yd, fd, st in
+              globals_min_ido xg &
+              yg == Nat.s xg &
+              fg == Nat.s yg &
+              xd == VarD (UnitT (Rd, MayWr), UnitE) &
+              yd == VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE xg) &
+              fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))],
+                          WriteS (DerefP (VarP 0))) &
+              prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
+              prog_evalo prog q })
+  (fun q -> q#reify (StEnv.prj_exn))))
+
+let prog_eval_t_simple_call_ref_wr _ = show(answer) (Stream.take (run q
+  (fun q -> ocanren {
+              fresh prog, xg, yg, fg, xd, yd, fd, st in
+              globals_min_ido xg &
+              yg == Nat.s xg &
+              fg == Nat.s yg &
+              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
+                          WriteS (DerefP (VarP 0))) &
+              prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
+              prog_evalo prog q })
+  (fun q -> q#reify (StEnv.prj_exn))))
+
+let prog_eval_t_simple_call_ref_fbd_wr _ = show(answer) (Stream.take (run q
+  (fun q -> ocanren {
+              fresh prog, xg, yg, fg, xd, yd, fd, st in
+              globals_min_ido xg &
+              yg == Nat.s xg &
+              fg == Nat.s yg &
+              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
+                          WriteS (DerefP (VarP 0))) &
+              prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
+                                               ReadS (DerefP (VarP yg)))) &
+              prog_evalo prog q })
+  (fun q -> q#reify (StEnv.prj_exn))))
+
+let prog_eval_t_simple_call_ref_wr_with_fix _ = show(answer) (Stream.take (run q
+  (fun q -> ocanren {
+              fresh prog, xg, yg, fg, xd, yd, fd, st in
+              globals_min_ido xg &
+              yg == Nat.s xg &
+              fg == Nat.s yg &
+              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
+                          WriteS (DerefP (VarP 0))) &
+              prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
+                                         SeqS (WriteS (DerefP (VarP yg)),
+                                               ReadS (DerefP (VarP yg))))) &
+              prog_evalo prog q })
+  (fun q -> q#reify (StEnv.prj_exn))))
+
+let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q
+  (fun q -> ocanren {
+              fresh prog, xg, yg, fg, f2g, xd, yd, fd, f2d, st in
+              globals_min_ido xg &
+              yg == Nat.s xg &
+              fg == Nat.s yg &
+              f2g == Nat.s fg &
+              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
+                          WriteS (DerefP (VarP 0))) &
+              f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))],
+                           SeqS (CallS (VarP f2g, [PathE (VarP 0)]),
+                                 WriteS (DerefP (VarP 0)))) &
+              prog == Prg ([xd; yd; fd], SeqS (CallS (VarP f2g, [PathE (VarP yg)]),
+                                               ReadS (DerefP (VarP yg)))) &
+              prog_evalo prog q })
+  (fun q -> q#reify (StEnv.prj_exn))))
+
+let prog_eval_t_fix_call_after_call _ = show(answer) (Stream.take (run q
+  (fun q -> ocanren {
+              fresh prog, xg, yg, fg, f2g, xd, yd, fd, f2d, st in
+              globals_min_ido xg &
+              yg == Nat.s xg &
+              fg == Nat.s yg &
+              f2g == Nat.s fg &
+              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
+                          WriteS (DerefP (VarP 0))) &
+              f2d == FunD ([(Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))],
+                           WriteS (DerefP (VarP 0))) &
+              prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
+                                         SeqS (CallS (VarP f2g, [PathE (VarP yg)]),
+                                               ReadS (DerefP (VarP yg))))) &
+              prog_evalo prog q })
+  (fun q -> q#reify (StEnv.prj_exn))))
+
+let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q
+  (fun q -> ocanren {
+              fresh prog, xg, yg, fg, xd, yd, fd, st in
+              globals_min_ido xg &
+              yg == Nat.s xg &
+              fg == Nat.s yg &
+              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
+                          SeqS (WriteS (VarP xg),
+                                ReadS (DerefP (VarP 0)))) &
+              prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
+                                               ReadS (DerefP (VarP yg)))) &
               prog_evalo prog q
               })
   (fun q -> q#reify (StEnv.prj_exn))))
 
+let prog_eval_t_call_with_rd_wr_2_args_ = show(answer) (Stream.take (run q
+  (fun q -> ocanren {
+              fresh prog, xg, yg, x2g, y2g, fg, xd, yd, x2d, y2d, fd, st in
+              globals_min_ido xg &
+              yg == Nat.s xg &
+              x2g == Nat.s yg &
+              y2g == Nat.s x2g &
+              fg == Nat.s y2g &
+              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              x2d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)));
+                           (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
+                          SeqS (ReadS (DerefP (VarP 0)),
+                                WriteS (DerefP (VarP 1)))) &
+              prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg); PathE (VarP y2g)])) &
+              prog_evalo prog q
+              })
+  (fun q -> q#reify (StEnv.prj_exn))))
+
+(* TODO: add tests to test file *)
+
 (* @type answerArgs = (Arg.ground List.ground) GT.list with show *)
 (* @type answerValue = Value.ground GT.list with show *)
 (* @type answerNat = Nat.ground GT.list with show *)