Fix buffer overflow for arity > 16 in Nary ops

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);

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):

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):