[Z3] Add option to manually validate Z3 models.

This can be enabled by passing the command line option `-debug-z3-validate-models`.
Although Z3 has a global parameter `model_validate` (off by default) I don't trust it
so do the validation manually. This also means we can potentially do
validation on a per Z3Solver instance basis rather than globally.

When failing to validate a Z3 model the solver state and model are
dumped to standard error.

1 files changed, 60 insertions, 0 deletions

diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index 311dbd12..c573011d 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -23,6 +23,10 @@ namespace {
 llvm::cl::opt<std::string> Z3QueryDumpFile(
     "debug-z3-dump-queries", llvm::cl::init(""),
     llvm::cl::desc("Dump Z3's representation of the query to the specified path"));
+
+llvm::cl::opt<bool> Z3ValidateModels(
+    "debug-z3-validate-models", llvm::cl::init(false),
+    llvm::cl::desc("When generating Z3 models validate these against the query"));
 }
 
 #include "llvm/Support/ErrorHandling.h"
@@ -43,6 +47,7 @@ private:
                          const std::vector<const Array *> *objects,
                          std::vector<std::vector<unsigned char> > *values,
                          bool &hasSolution);
+bool validateZ3Model(::Z3_solver &theSolver, ::Z3_model &theModel);
 
 public:
   Z3SolverImpl();
@@ -306,6 +311,13 @@ SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse(
       values->push_back(data);
     }
 
+    // Validate the model if requested
+    if (Z3ValidateModels) {
+      bool success = validateZ3Model(theSolver, theModel);
+      if (!success)
+        abort();
+    }
+
     Z3_model_dec_ref(builder->ctx, theModel);
     return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
   }
@@ -330,6 +342,54 @@ SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse(
   }
 }
 
+bool Z3SolverImpl::validateZ3Model(::Z3_solver &theSolver, ::Z3_model &theModel) {
+  bool success = true;
+  ::Z3_ast_vector constraints =
+      Z3_solver_get_assertions(builder->ctx, theSolver);
+  Z3_ast_vector_inc_ref(builder->ctx, constraints);
+
+  unsigned size = Z3_ast_vector_size(builder->ctx, constraints);
+
+  for (unsigned index = 0; index < size; ++index) {
+    Z3ASTHandle constraint = Z3ASTHandle(
+        Z3_ast_vector_get(builder->ctx, constraints, index), builder->ctx);
+
+    ::Z3_ast rawEvaluatedExpr;
+    bool successfulEval =
+        Z3_model_eval(builder->ctx, theModel, constraint,
+                      /*model_completion=*/Z3_TRUE, &rawEvaluatedExpr);
+    assert(successfulEval && "Failed to evaluate model");
+
+    // Use handle to do ref-counting.
+    Z3ASTHandle evaluatedExpr(rawEvaluatedExpr, builder->ctx);
+
+    Z3SortHandle sort =
+        Z3SortHandle(Z3_get_sort(builder->ctx, evaluatedExpr), builder->ctx);
+    assert(Z3_get_sort_kind(builder->ctx, sort) == Z3_BOOL_SORT &&
+           "Evaluated expression has wrong sort");
+
+    Z3_lbool evaluatedValue =
+        Z3_get_bool_value(builder->ctx, evaluatedExpr);
+    if (evaluatedValue != Z3_L_TRUE) {
+      llvm::errs() << "Validating model failed:\n"
+                   << "The expression:\n";
+      constraint.dump();
+      llvm::errs() << "evaluated to \n";
+      evaluatedExpr.dump();
+      llvm::errs() << "But should be true\n";
+      success = false;
+    }
+  }
+
+  if (!success) {
+    llvm::errs() << "Solver state:\n" << Z3_solver_to_string(builder->ctx, theSolver) << "\n";
+    llvm::errs() << "Model:\n" << Z3_model_to_string(builder->ctx, theModel) << "\n";
+  }
+
+  Z3_ast_vector_dec_ref(builder->ctx, constraints);
+  return success;
+}
+
 SolverImpl::SolverRunStatus Z3SolverImpl::getOperationStatusCode() {
   return runStatusCode;
 }