diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 039f8e5..248e366 100644 --- a/model_with_structures/analyzer.ml +++ b/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: FIXME: check *) + (* TODO: 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))])); *) diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index e34ddc2..b100a82 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -482,11 +482,14 @@ struct v == RefV id & tp == RefT (c, tp') & { { c == Rf & mem_with_id' == Std.pair mem v } | - { fresh v', mem_cp, v_cp, mem_add, id_add in + { fresh v, mem_cp, v_cp, mem_with_v_cp, + mem_add, id_add, mem_with_id_add in c == Cp & - mem_geto mem id v' & - valcopyo mem v' tp' (Std.pair mem_cp v_cp) & - mem_addo mem_cp v_cp (Std.pair mem_add id_add) & + mem_geto mem id v & + valcopyo mem v tp mem_with_v_cp & + Std.pair mem v_cp == mem_with_v_cp & + 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 & @@ -878,9 +881,7 @@ struct (* TODO: FIXME check left or right order *) list_foldl2o (stmt_eval_spoil_foldero types vals) mem tps es mem_spoiled & - (* st' == state_with_args *) - st' == StEnv (mem_spoiled, types, vals) - } | + st' == StEnv (mem_spoiled, types, vals) } | { fresh p, tp, _r, w, x, id, v, mem_upd, v_upd, mem_set in s == WriteS p & diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index 416a361..f82b186 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -24,24 +24,6 @@ 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))]] |}] *) diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index ad1e3b8..69a5113 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -10,7 +10,6 @@ open Decl open Type open Expr open Path -open CopyCap open ReadCap open WriteCap open InCap @@ -110,189 +109,10 @@ 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 *)