diff --git a/harmony_model_checker/charm/ops.c b/harmony_model_checker/charm/ops.c index b0e1a6ae..b6724c38 100644 --- a/harmony_model_checker/charm/ops.c +++ b/harmony_model_checker/charm/ops.c @@ -2477,6 +2477,7 @@ void op_Nary(const void *env, struct state *state, struct step *step){ } } } + assert(en->arity <= MAX_ARITY); for (unsigned int i = 0; i < en->arity; i++) { args[i] = ctx_pop(step->ctx); if (step->keep_callstack) { @@ -3422,6 +3423,10 @@ void *init_Nary(struct dict *map, struct allocator *allocator){ copy[arity->u.atom.len] = 0; env->arity = atoi(copy); free(copy); + if (env->arity > MAX_ARITY) { + fprintf(stderr, "Nary: arity %u is too large (> %u)\n", env->arity, MAX_ARITY); + exit(1); + } struct json_value *op = dict_lookup(map, "value", 5); assert(op->type == JV_ATOM); diff --git a/harmony_model_checker/harmony/ast.py b/harmony_model_checker/harmony/ast.py index 3e953b08..a43467f4 100644 --- a/harmony_model_checker/harmony/ast.py +++ b/harmony_model_checker/harmony/ast.py @@ -666,6 +666,16 @@ def gencode(self, scope, code, stmt): else: for i in range(n): self.args[i].compile(scope, code, stmt) + # TODO: in the future maybe split into chunks of smaller arity + if n > NaryOp.MAX_ARITY: + lexeme, file, line, column = self.endtoken # end token looks better imo + raise HarmonyCompilerError( + message="Arity %d exceeds max arity %d" % (n, NaryOp.MAX_ARITY), + filename=file, + line=line, + column=column, + lexeme=lexeme + ) code.append(NaryOp(self.op, n), self.token, self.endtoken, stmt=stmt) def getLabels(self): diff --git a/harmony_model_checker/harmony/ops.py b/harmony_model_checker/harmony/ops.py index 7e129ac4..7ebbe29c 100644 --- a/harmony_model_checker/harmony/ops.py +++ b/harmony_model_checker/harmony/ops.py @@ -1260,8 +1260,13 @@ def substitute(self, map): self.pc = map[self.pc].pc class NaryOp(Op): + # See MAX_ARITY in `ops.c` + MAX_ARITY = 16 + def __init__(self, op, n): + """Caller should check that n <= MAX_ARITY""" self.op = op + assert n <= self.MAX_ARITY self.n = n def __repr__(self):