Merge pull request #624 from SRI-CSL/fix-issue-615-interpolation-crash

Fix issue #615: crash in mcsat_value_construct_from_value during interpolation.

Author: disteph

src/api/yices_api.c

@@ -2534,6 +2534,63 @@ static bool check_good_vars_or_uninterpreted(term_manager_t *mngr, uint32_t n, c
   return true;
 }
 
+static bool mcsat_assumption_type_supported(type_table_t *types, type_t tau) {
+  type_kind_t kind = type_kind(types, tau);
+  uint32_t i;
+
+  switch (kind) {
+  case BOOL_TYPE:
+  case INT_TYPE:
+  case REAL_TYPE:
+  case SCALAR_TYPE:
+  case BITVECTOR_TYPE:
+    return true;
+
+  case TUPLE_TYPE: {
+    tuple_type_t *tuple = tuple_type_desc(types, tau);
+    for (i = 0; i < tuple->nelem; i++) {
+      if (! mcsat_assumption_type_supported(types, tuple->elem[i])) {
+        return false;
+      }
+    }
+    return true;
+  }
+
+  default:
+    return false;
+  }
+}
+
+// Check that the type of every term in v is one that the MCSAT solver can
+// decide on as an assumption value. Tuple types are supported if all their
+// recursively flattened leaves are supported scalar decision types. Other
+// type kinds (UNINTERPRETED_TYPE, FUNCTION_TYPE, FF_TYPE, etc.) reach the
+// MCSAT solver but trigger an assertion failure inside
+// mcsat_value_construct_from_value (or a NULL decide_assignment dispatch),
+// so we reject them here with a clear error code (issue #615).
+//
+// All elements of v must already be good terms.
+static bool check_mcsat_assumption_types(term_manager_t *mngr, uint32_t n, const term_t *v) {
+  term_table_t *tbl;
+  type_table_t *types;
+  uint32_t i;
+
+  tbl = term_manager_get_terms(mngr);
+  types = tbl->types;
+  for (i=0; i<n; i++) {
+    type_t tau = term_type(tbl, v[i]);
+    if (! mcsat_assumption_type_supported(types, tau)) {
+      error_report_t *error = get_yices_error();
+      error->code = MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED;
+      error->term1 = v[i];
+      error->type1 = tau;
+      return false;
+    }
+  }
+
+  return true;
+}
+
 // Check whether arrays v and a define a valid substitution
 // both must be arrays of n elements
 static bool check_good_substitution(term_manager_t *mngr, uint32_t n, const term_t *v, const term_t *a) {
@@ -9571,6 +9628,18 @@ static bool good_terms_for_check_with_model(uint32_t n, const term_t t[]) {
   MT_PROTECT(bool, __yices_globals.lock, _o_good_terms_for_check_with_model(n, t));
 }
 
+/*
+ * Same as _o_good_terms_for_check_with_model, but additionally checks that
+ * the type of each assumption term is one MCSAT can decide on. This guards
+ * against the crash reported in issue #615. Tuple assumptions are allowed
+ * only if every recursively flattened leaf type is supported by an MCSAT
+ * decision plugin.
+ */
+static bool _o_good_assumption_terms_for_mcsat(uint32_t n, const term_t t[]) {
+  return _o_good_terms_for_check_with_model(n, t)
+      && check_mcsat_assumption_types(__yices_globals.manager, n, t);
+}
+
 /*
  * Check context with model
  * - param = parameter for check sat (or NULL for default parameters)
@@ -9588,10 +9657,16 @@ static smt_status_t _o_yices_check_context_with_model(context_t *ctx, const para
     return YICES_STATUS_ERROR;
   }
 
-  if (! _o_good_terms_for_check_with_model(n, t)) {
-    // this sets the error code already (to VARIABLE_REQUIRED)
-    // but Dejan created another error code that means the same thing here.
-    set_error_code(MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED);
+  if (! _o_good_assumption_terms_for_mcsat(n, t)) {
+    // Normalize the error code: VARIABLE_REQUIRED (set by the
+    // term-shape check) becomes MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED,
+    // matching the long-standing convention here. The new
+    // MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED (set by the type-kind
+    // check) is left as-is so callers can distinguish "wrong shape" from
+    // "wrong type". term1/type1 fields are preserved.
+    if (yices_error_code() == VARIABLE_REQUIRED) {
+      set_error_code(MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED);
+    }
     return YICES_STATUS_ERROR;
   }
 
@@ -9669,10 +9744,11 @@ static smt_status_t _o_yices_check_context_with_model_and_hint(context_t *ctx, c
     return YICES_STATUS_ERROR;
   }
 
-  if (! _o_good_terms_for_check_with_model(n, t)) {
-    // this sets the error code already (to VARIABLE_REQUIRED)
-    // but Dejan created another error code that means the same thing here.
-    set_error_code(MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED);
+  if (! _o_good_assumption_terms_for_mcsat(n, t)) {
+    // See note in _o_yices_check_context_with_model.
+    if (yices_error_code() == VARIABLE_REQUIRED) {
+      set_error_code(MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED);
+    }
     return YICES_STATUS_ERROR;
   }
 
@@ -9880,16 +9956,28 @@ EXPORTED smt_status_t yices_check_context_with_interpolation(interpolation_conte
     ctx->model = yices_get_model(ctx->ctx_A, true);
   }
 
-  // Pop both contexts
-  if (result != YICES_STATUS_ERROR) {
+  // Pop both contexts. Preserve the original error report if the loop above
+  // failed (for example, via model-refutation assumption validation).
+  {
+    bool preserve_error = result == YICES_STATUS_ERROR;
+    error_report_t saved_error;
+    if (preserve_error) {
+      saved_error = *get_yices_error();
+    }
+
     ret = yices_pop(ctx->ctx_B);
-    if (ret) {
+    if (ret && !preserve_error) {
       result = YICES_STATUS_ERROR;
-    } else {
-      ret = yices_pop(ctx->ctx_A);
-      if (ret) {
-        result = YICES_STATUS_ERROR;
-      }
+    }
+    // Pop A even if popping B failed: both contexts were pushed above and
+    // must be balanced independently.
+    ret = yices_pop(ctx->ctx_A);
+    if (ret && !preserve_error) {
+      result = YICES_STATUS_ERROR;
+    }
+
+    if (preserve_error) {
+      *get_yices_error() = saved_error;
     }
   }
 

src/api/yices_error.c

@@ -608,6 +608,10 @@ int32_t print_error(FILE *f) {
     code = fprintf(f, "mcsat: checking with assumptions only supports variables as assumptions\n");
     break;
 
+  case MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED:
+    code = fprintf(f, "mcsat: assumption variable has a type that mcsat cannot decide on\n");
+    break;
+
   case INTERNAL_EXCEPTION:
   default:
     code = fprintf(f, "internal error\n");
@@ -1137,6 +1141,10 @@ char *error_string(void) {
     nchar = snprintf(buffer, BUFFER_SIZE,  "mcsat: checking with assumptions only supports variables as assumptions\n");
     break;
 
+  case MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED:
+    nchar = snprintf(buffer, BUFFER_SIZE,  "mcsat: assumption variable has a type that mcsat cannot decide on\n");
+    break;
+
   case INTERNAL_EXCEPTION:
   default:
     nchar = snprintf(buffer, BUFFER_SIZE, "internal error");

src/frontend/smt2/smt2_commands.c

@@ -1102,6 +1102,10 @@ static void print_yices_error(bool full) {
     print_out("mcsat: checking with assumptions only supports variables as assumptions");
     break;
 
+  case MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED:
+    print_out("mcsat: assumption variable has a type that mcsat cannot decide on");
+    break;
+
   case OUTPUT_ERROR:
     print_out(" IO error");
     break;

src/include/yices.h

@@ -3370,6 +3370,11 @@ __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_assumptions(conte
  * if one of the terms t[i] is not an uninterpreted term
  *   code = MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED
  *
+ * if one of the terms t[i] has a type that MCSAT cannot decide on
+ * (i.e. not Bool, Int, Real, scalar, BitVector, or a tuple whose
+ * recursively flattened leaves all have one of these types)
+ *   code = MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED
+ *
  * If the context does not have the MCSAT solver enabled
  *   code = CTX_OPERATION_NOT_SUPPORTED
  *
@@ -3418,6 +3423,11 @@ __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_model(context_t *
  * if one of the terms t[i] is not an uninterpreted term
  *   code = MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED
  *
+ * if one of the terms t[i] has a type that MCSAT cannot decide on
+ * (i.e. not Bool, Int, Real, scalar, BitVector, or a tuple whose
+ * recursively flattened leaves all have one of these types)
+ *   code = MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED
+ *
  * If the context does not have the MCSAT solver enabled
  *   code = CTX_OPERATION_NOT_SUPPORTED
  *
@@ -3506,8 +3516,9 @@ __YICES_DLLSPEC__ extern smt_status_t yices_mcsat_set_initial_var_order(context_
  * a model is returned in ctx->model. This model must be freed when no-longer needed by
  * calling yices_free_model.
  *
- * If something is wrong, the function returns YICES_STATUS_ERROR and sets the yices error report
- * (code = CTX_INVALID_OPERATION).
+ * If something is wrong, the function returns YICES_STATUS_ERROR and sets the yices error report.
+ * This includes CTX_INVALID_OPERATION and any error propagated from the internal
+ * yices_check_context_with_model call used for model refutation.
  *
  * Since 2.6.4.
  */

src/include/yices_types.h

@@ -480,6 +480,7 @@ typedef enum error_code {
    */
   MCSAT_ERROR_UNSUPPORTED_THEORY = 1000,
   MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED = 1001,
+  MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED = 1002,
 
   /*
    * Input/output and system errors

src/mcsat/preprocessor.c

@@ -2397,6 +2397,12 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is
   return t_pre;
 }
 
+void preprocessor_tuple_blast(preprocessor_t* pre, term_t t, ivector_t* out) {
+  ivector_reset(out);
+  tuple_blast_term(pre, t);
+  tuple_blast_get(pre, t, out);
+}
+
 void preprocessor_set_exception_handler(preprocessor_t* pre, jmp_buf* handler) {
   pre->exception = handler;
 }

src/mcsat/preprocessor.h

@@ -111,6 +111,14 @@ void preprocessor_destruct(preprocessor_t* pre);
 /** Preprocess the term, add any additional assertions to output vector. */
 term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is_assertion);
 
+/*
+ * Tuple-blast term t and copy its flattened leaves into out.
+ * - out is reset first.
+ * - leaf order matches type_collect_blasted_atom_types/type leaf order.
+ * - leaves are memoized and stable across later tuple-blast calls.
+ */
+void preprocessor_tuple_blast(preprocessor_t* pre, term_t t, ivector_t* out);
+
 /** Set tracer */
 void preprocessor_set_tracer(preprocessor_t* pre, tracer_t* tracer);