From 279a548a58c022df534938c249750a28c155f5ed Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Tue, 12 May 2026 17:42:54 +0000 Subject: [PATCH] struct: first attempt to synt in complex example, functions to omit capabilities --- model_with_structures/synthesizer.ml | 7 - model_with_structures/tests.ml | 2 + model_with_structures/tests_f.ml | 215 ++++++++++++++++++++++++++- 3 files changed, 215 insertions(+), 9 deletions(-) diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index b4c1972..57b4207 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -1033,11 +1033,4 @@ struct prog_inito prog init_st & stmt_evalo init_st s st' } - - (* --- tests --- *) - (* TODO *) - - (* - shortcuts *) - (* TODO *) - end diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index d03bad1..db667a7 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -85,4 +85,6 @@ let%expect_test "simple synthesis test, reference forbidden write, no read write let%expect_test "complex test: send" = print_endline(prog_eval_compl_test_send ()); [%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)))))))))]); FunV ([SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O))))))))]); FunV ([SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O)))))]); FunV ([ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS)]); TupleV ([RefV (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))); RefV (S (S (S (S (S (S (S (S (S (S (O))))))))))); RefV (S (S (S (S (S (S (S (S (S (O)))))))))); RefV (S (S (S (S (S (S (S (S (O))))))))); ZeroV]); TupleV ([RefV (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))); RefV (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))]); TupleV ([ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV]); ZeroV; ZeroV; TupleV ([ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([RefV (S (S (S (O)))); RefV (S (S (O)))]); TupleV ([ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV])], S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr)); UnitT (Rd, AlwaysWr)])); (S (S (S (S (S (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 (S (S (O)))))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr)); UnitT (Rd, AlwaysWr)])); (S (S (S (S (S (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 (S (S (O)))))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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 (S (S (S (S (S (S (S (S (O)))))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)]), VisitedEnv ([SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))))); ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))))); ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)))))))))]))] |}] +let%expect_test "complex test: send" = print_endline(prog_synt_compl_test_send ()); + [%expect {| [Cp] |}] (* TODO *) diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index fbfe3eb..253af34 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -21,6 +21,8 @@ open Mode StEnv.ground GT.list with show @type answerCpCap = CopyCap.ground GT.list with show +@type answerCpCapVec = + (CopyCap.ground GT.list) GT.list with show (* - shortcuts *) @@ -518,7 +520,6 @@ let access_deref_access_deref_accesso id_ext id_mid id_int v p' = ocanren { p' == AccessP (DerefP (AccessP (DerefP (AccessP (VarP v, id_int)), id_mid)), id_ext) } -(* TODO *) let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q (fun q -> ocanren { fresh (* types *) @@ -654,4 +655,214 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) -(* TODO: + synth. test *) +let any_unitTo tp = ocanren { + fresh r, w in + tp == UnitT (r, w) + } + +let any_user_utilsTo tp = ocanren { + fresh x, y in + any_unitTo x & + any_unitTo y & + tp == TupleT [x; y] + } + +let any_user_infoTo tp = ocanren { + fresh x, y, z in + any_unitTo x & + any_unitTo y & + any_unitTo z & + tp == TupleT [x; y; z] + } + +let any_versionTo tp = ocanren { + fresh x, y, z in + any_unitTo x & + any_unitTo y & + any_unitTo z & + tp == TupleT [x; y; z] + } + +let any_utilsTo tp = ocanren { + fresh x, y in + any_unitTo x & + any_unitTo y & + tp == TupleT [x; y] + } + +let any_dataTo tp = ocanren { + any_unitTo tp + } + +let any_op_dateTo tp = ocanren { + any_unitTo tp + } + +let any_userTo cu ci tp = ocanren { + fresh utilsT, infoT in + any_user_infoTo infoT & + any_user_utilsTo utilsT & + tp == TupleT [RefT (cu, utilsT) (* 0 utils *); + RefT (ci, infoT) (* 1 info *)] + } + +let any_requestTo cus cv cut cd cus_u cus_i tp = ocanren { + fresh userT, versionT, utilsT, dataT, op_dateT in + any_userTo cus_u cus_i userT & + any_versionTo versionT & + any_utilsTo utilsT & + any_dataTo dataT & + any_op_dateTo op_dateT & + tp == TupleT [RefT (cus, userT) (* 0 user *); + RefT (cv, versionT) (* 1 version *); + RefT (cut, utilsT) (* 2 utils *); + RefT (cd, dataT) (* 3 data *); + op_dateT (* 4 operation_date *)] + } +let any_moded_requestTo cus cv cut cd cus_u cus_i tp = ocanren { + fresh requestT in + any_requestTo cus cv cut cd cus_u cus_i requestT & + tp == (Mode (In, NOut), requestT) + } +let any_boxed_moded_requestTo tp = ocanren { + fresh cus, cv, cut, cd, cus_u, cus_i in + any_moded_requestTo cus cv cut cd cus_u cus_i tp + } + +(* TODO: synt all modifiers, etc *) +let prog_synt_compl_test_send _ = show(answerCpCap) (Stream.take (run q + (fun q -> ocanren { + fresh (* types *) + uT_r_aw, + user_utilsT, user_infoT, + userT, versionT, utilsT, + requestT, + moded_requestT, + (* global vars init exprs *) + user_utilsE, user_infoE, + userE, versionE, utilsE, + requestE, + (* global vars ids *) + user_utilsID, user_infoID, + userID, versionID, utilsID, + dataID, requestID, + (* function ids *) + get_version_idID, + updated_versionID, + sendID, + send_allID, + (* function definitions *) + get_version_idF, + updated_versionF, + sendFBranch, + sendF, + send_allF, + (* other *) + prog, + (* synt *) + st in + (* types *) + uT_r_aw == UnitT (Rd, AlwaysWr) & + user_utilsT == TupleT [uT_r_aw (* 0 id *); uT_r_aw] & + user_infoT == TupleT [uT_r_aw (* 0 name *); uT_r_aw; uT_r_aw] & + userT == TupleT [RefT (q, user_utilsT) (* 0 utils *); + RefT (Cp, user_infoT) (* 1 info *)] & + versionT == TupleT [uT_r_aw (* 0 id *); uT_r_aw; uT_r_aw] & + utilsT == TupleT [uT_r_aw (* 0 has_version *); uT_r_aw (* 1 id *)] & + requestT == TupleT [RefT (Cp, userT) (* 0 user *); + RefT (Cp, versionT) (* 1 version *); + RefT (Cp, utilsT) (* 2 utils *); + RefT (Cp, uT_r_aw) (* 3 data *); + uT_r_aw (* 4 operation_date *)] & + moded_requestT == (Mode (In, NOut), requestT) & + (* global vars init exprs *) + user_utilsE == TupleE [UnitE (* 0 id *); UnitE] & + user_infoE == TupleE [UnitE (* 0 name *); UnitE; UnitE] & + userE == TupleE [RefE user_utilsID (* 0 utils *); + RefE user_infoID (* 1 info *)] & + versionE == TupleE [UnitE (* 0 id *); UnitE; UnitE] & + utilsE == TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] & + requestE == TupleE [RefE userID (* 0 user *); + RefE versionID (* 1 version *); + RefE utilsID (* 2 utils *); + RefE dataID (* 3 data *); + UnitE (* 4 operation_date *)] & + (* global vars ids *) + globals_min_ido user_utilsID & + user_infoID == Nat.s user_utilsID & + userID == Nat.s user_infoID & + versionID == Nat.s userID & + utilsID == Nat.s versionID & + dataID == Nat.s utilsID & + requestID == Nat.s dataID & + (* function ids *) + get_version_idID == Nat.s requestID & + updated_versionID == Nat.s get_version_idID & + sendID == Nat.s updated_versionID & + send_allID == Nat.s sendID & + (* function definitions *) + fresh gvi_access0 in + access_deref_accesso 0 1 0 gvi_access0 & + get_version_idF == ChoiceS (ReadS gvi_access0, SkipS) & + + fresh uv_access0, uv_access1, uv_access2 in + access_deref_accesso 0 2 0 uv_access0 & + access_deref_accesso 0 1 0 uv_access1 & + access_deref_accesso 1 1 0 uv_access2 & + seqo [ReadS uv_access0; + ReadS uv_access1; + ReadS uv_access2] + updated_versionF & + + fresh sb_access0, sb_access1, sb_access2, sb_access3 in + access_deref_accesso 0 2 0 sb_access0 & + deref_accesso 3 0 sb_access1 & + deref_accesso 3 0 sb_access2 & + access_deref_access_deref_accesso 0 1 0 0 sb_access3 & + seqo [WriteS sb_access0; + ReadS sb_access1; + WriteS sb_access2; + ReadS sb_access3] + sendFBranch & + seqo [ChoiceS (sendFBranch, SkipS); + WriteS (AccessP (VarP 0, 4)); + (* TODO: read all the substructure ?? *) + ReadS (AccessP (VarP 0, 4)) (*rdS v0*)] (* FIXME: TMP, parial read, should be full *) + sendF & + + fresh sa_access0, sa_access1, sa_access2, sa_access3 in + access_deref_accesso 0 1 0 sa_access0 & + access_deref_accesso 1 1 0 sa_access1 & + access_deref_access_deref_accesso 0 0 0 0 sa_access2 & + access_deref_accesso 0 1 0 sa_access3 & + seqo [WriteS (AccessP (VarP 0, 4)) (*wrS v0*); (* FIXME: TMP, parial write, should be full *) + CallS (VarP sendID, [PathE (VarP 0)]); + CallS (VarP get_version_idID, [PathE (VarP 0)]); + CallS (VarP updated_versionID, [PathE (VarP 0)]); + (* TODO: read all the substructure ?? *) + WriteS sa_access0; + WriteS sa_access1; + ChoiceS ( + ReadS sa_access2, + ReadS sa_access3 + )] + send_allF & + + prog == Prg ([ + VarD (user_utilsT, user_utilsE); + VarD (user_infoT, user_infoE); + VarD (userT, userE); + VarD (versionT, versionE); + VarD (utilsT, utilsE); + VarD (uT_r_aw, UnitE); (* data *) + VarD (requestT, requestE); + FunD ([moded_requestT], get_version_idF); + FunD ([moded_requestT], updated_versionF); + FunD ([moded_requestT], sendF); + FunD ([moded_requestT], send_allF) + ], + (* SkipS *) + CallS (VarP send_allID, [PathE (VarP requestID)]) + ) & + prog_evalo prog st }) + (fun q -> q#reify (CopyCap.prj_exn)))) (* TODO: list *)