external/ton
1
0
Fork 0
mirror of https://github.com/ton-blockchain/ton synced 2025-03-09 15:40:10 +00:00
Code Issues Releases Wiki Activity

FunC: Prohibit unifying tensors and "forall" vars (#684)

Browse source 
* FunC: Prohibit unifying tensors and "forall" vars

* Bump funC version to 0.4.4

---------

Co-authored-by: SpyCheese <mikle98@yandex.ru>
This commit is contained in:
EmelyanenkoK 2023-04-27 10:23:04 +03:00 • committed by GitHub
parent aab1fe0751
commit 5606418234
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 24 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

5
crypto/func/func.h
View file

@ -41,7 +41,7 @@ extern std::string generated_from;
constexpr int optimize_depth = 20; constexpr int optimize_depth = 20;
const std::string func_version{"0.4.3"}; const std::string func_version{"0.4.4"};
enum Keyword { enum Keyword {
_Eof = -1, _Eof = -1,
@ -159,6 +159,7 @@ struct TypeExpr {
int minw, maxw; int minw, maxw;
static constexpr int w_inf = 1023; static constexpr int w_inf = 1023;
std::vector<TypeExpr*> args; std::vector<TypeExpr*> args;
bool was_forall_var = false;
TypeExpr(te_type _constr, int _val = 0) : constr(_constr), value(_val), minw(0), maxw(w_inf) { TypeExpr(te_type _constr, int _val = 0) : constr(_constr), value(_val), minw(0), maxw(w_inf) {
} }
TypeExpr(te_type _constr, int _val, int width) : constr(_constr), value(_val), minw(width), maxw(width) { TypeExpr(te_type _constr, int _val, int width) : constr(_constr), value(_val), minw(width), maxw(width) {
@ -265,7 +266,7 @@ struct TypeExpr {
return new TypeExpr{te_ForAll, body, std::move(list)}; return new TypeExpr{te_ForAll, body, std::move(list)};
} }
static bool remove_indirect(TypeExpr*& te, TypeExpr* forbidden = nullptr); static bool remove_indirect(TypeExpr*& te, TypeExpr* forbidden = nullptr);
static bool remove_forall(TypeExpr*& te); static std::vector<TypeExpr*> remove_forall(TypeExpr*& te);
static bool remove_forall_in(TypeExpr*& te, TypeExpr* te2, const std::vector<TypeExpr*>& new_vars); static bool remove_forall_in(TypeExpr*& te, TypeExpr* te2, const std::vector<TypeExpr*>& new_vars);
}; };

31
crypto/func/unify-types.cpp
View file

@ -146,11 +146,8 @@ bool TypeExpr::remove_indirect(TypeExpr*& te, TypeExpr* forbidden) {
return res; return res;
} }
bool TypeExpr::remove_forall(TypeExpr*& te) { std::vector<TypeExpr*> TypeExpr::remove_forall(TypeExpr*& te) {
assert(te); assert(te && te->constr == te_ForAll);
if (te->constr != te_ForAll) {
return false;
}
assert(te->args.size() >= 1); assert(te->args.size() >= 1);
std::vector<TypeExpr*> new_vars; std::vector<TypeExpr*> new_vars;
for (std::size_t i = 1; i < te->args.size(); i++) { for (std::size_t i = 1; i < te->args.size(); i++) {
@ -161,7 +158,7 @@ bool TypeExpr::remove_forall(TypeExpr*& te) {
te = te->args[0]; te = te->args[0];
remove_forall_in(te, te2, new_vars); remove_forall_in(te, te2, new_vars);
// std::cerr << "-> " << te << std::endl; // std::cerr << "-> " << te << std::endl;
return true; return new_vars;
} }
bool TypeExpr::remove_forall_in(TypeExpr*& te, TypeExpr* te2, const std::vector<TypeExpr*>& new_vars) { bool TypeExpr::remove_forall_in(TypeExpr*& te, TypeExpr* te2, const std::vector<TypeExpr*>& new_vars) {
@ -363,20 +360,34 @@ void unify(TypeExpr*& te1, TypeExpr*& te2) {
} }
if (te1->constr == TypeExpr::te_ForAll) { if (te1->constr == TypeExpr::te_ForAll) {
TypeExpr* te = te1; TypeExpr* te = te1;
if (!TypeExpr::remove_forall(te)) { std::vector<TypeExpr*> new_vars = TypeExpr::remove_forall(te);
throw UnifyError{te1, te2, "cannot remove universal type quantifier while performing type unification"}; for (TypeExpr* t : new_vars) {
t->was_forall_var = true;
} }
unify(te, te2); unify(te, te2);
for (TypeExpr* t : new_vars) {
t->was_forall_var = false;
}
return; return;
} }
if (te2->constr == TypeExpr::te_ForAll) { if (te2->constr == TypeExpr::te_ForAll) {
TypeExpr* te = te2; TypeExpr* te = te2;
if (!TypeExpr::remove_forall(te)) { std::vector<TypeExpr*> new_vars = TypeExpr::remove_forall(te);
throw UnifyError{te2, te1, "cannot remove universal type quantifier while performing type unification"}; for (TypeExpr* t : new_vars) {
t->was_forall_var = true;
} }
unify(te1, te); unify(te1, te);
for (TypeExpr* t : new_vars) {
t->was_forall_var = false;
}
return; return;
} }
if (te1->was_forall_var && te2->constr == TypeExpr::te_Tensor) {
throw UnifyError{te1, te2, "cannot unify generic type and tensor"};
}
if (te2->was_forall_var && te1->constr == TypeExpr::te_Tensor) {
throw UnifyError{te2, te1, "cannot unify generic type and tensor"};
}
if (te1->constr == TypeExpr::te_Unknown) { if (te1->constr == TypeExpr::te_Unknown) {
if (te2->constr == TypeExpr::te_Unknown) { if (te2->constr == TypeExpr::te_Unknown) {
assert(te1->value != te2->value); assert(te1->value != te2->value);