Enhance type error understanding by displaying incompatible constraints

CMakeLists.txt

@@ -6,6 +6,8 @@
 
 cmake_minimum_required(VERSION 3.15)
 
+set(CMAKE_CXX_STANDARD 17)
+
 include(CMakeDependentOption)
 
 option(SOUFFLE_GIT "Enable/Disable git completion" ON)

src/TranslationUnitBase.h

@@ -22,6 +22,7 @@
 #include "souffle/utility/DynamicCasting.h"
 #include "souffle/utility/Types.h"
 #include <cassert>
+#include <cstring>
 #include <map>
 #include <memory>
 #include <ostream>
@@ -88,7 +89,7 @@ struct TranslationUnitBase {
             it = analyses.insert({A::name, mk<A>()}).first;
 
             auto& analysis = *it->second;
-            assert(analysis.getName() == A::name && "must be same pointer");
+            assert((std::strcmp(analysis.getName(), A::name) == 0) && "must be same pointer");
             analysis.run(static_cast<Impl const&>(*this));
             logAnalysis(analysis);
         }

src/ast/analysis/Constraint.h

@@ -17,6 +17,8 @@
 #pragma once
 
 #include "ConstraintSystem.h"
+#include "ErrorAnalyzer.h"
+#include "ValueChecker.h"
 #include "ast/Argument.h"
 #include "ast/Clause.h"
 #include "ast/Node.h"
@@ -44,6 +46,12 @@ struct ConstraintAnalysisVar : public Variable<const Argument*, PropertySpace> {
     void print(std::ostream& out) const override {
         out << "var(" << *(this->id) << ")";
     }
+
+    const std::string name() const {
+        std::stringstream ss;
+        ss << *(this->id);
+        return ss.str();
+    }
 };
 
 /**
@@ -55,11 +63,12 @@ struct ConstraintAnalysisVar : public Variable<const Argument*, PropertySpace> {
  *      to be utilized by this analysis.
  */
 template <typename AnalysisVar>
-class ConstraintAnalysis : public Visitor<void> {
+class ConstraintAnalysis : public Visitor<void>, ValueChecker<AnalysisVar> {
 public:
     using value_type = typename AnalysisVar::property_space::value_type;
     using constraint_type = std::shared_ptr<Constraint<AnalysisVar>>;
     using solution_type = std::map<const Argument*, value_type>;
+    using error_analyzer_type = ErrorAnalyzer<AnalysisVar>;
 
     virtual void collectConstraints(const Clause& clause) {
         visit(clause, *this);
@@ -72,7 +81,9 @@ class ConstraintAnalysis : public Visitor<void> {
      * @param debug a flag enabling the printing of debug information
      * @return an assignment mapping a property to each argument in the given clause
      */
-    solution_type analyse(const Clause& clause, std::ostream* debugOutput = nullptr) {
+    solution_type analyse(const Clause& clause, error_analyzer_type* errorAnalyzer = nullptr,
+            std::ostream* debugOutput = nullptr) {
+        this->errorAnalyzer = errorAnalyzer;
         collectConstraints(clause);
 
         assignment = constraints.solve();
@@ -84,9 +95,29 @@ class ConstraintAnalysis : public Visitor<void> {
             *debugOutput << "Solution:\n" << assignment << "\n";
         }
 
+        if (errorAnalyzer) {
+            std::map<AnalysisVar, typename Problem<AnalysisVar>::unsat_core_type> unsat_cores;
+            for (const auto& [arg, value] : assignment) {
+                if (!this->valueIsValid(value)) {
+                    auto unsat_core = constraints.extractUnsatCore(arg);
+                    unsat_cores[arg] = unsat_core;
+                }
+            }
+            std::map<AnalysisVar, std::set<const Argument*>> equivalentArguments;
+            visit(clause, [&](const Argument& arg) {
+                errorAnalyzer->addUnsatCore(&arg, unsat_cores[getVar(arg)]);
+                equivalentArguments[getVar(arg)].emplace(&arg);
+            });
+            for (const auto& [_, argSet] : equivalentArguments) {
+                errorAnalyzer->addEquivalentArgumentSet(argSet);
+            }
+        }
+
         // convert assignment to result
         solution_type solution;
         visit(clause, [&](const Argument& arg) { solution[&arg] = assignment[getVar(arg)]; });
+
+        this->errorAnalyzer = nullptr;
         return solution;
     }
 
@@ -131,6 +162,8 @@ class ConstraintAnalysis : public Visitor<void> {
 
     /** A map mapping variables to unique instances to facilitate the unification of variables */
     std::map<std::string, AnalysisVar> variables;
+
+    error_analyzer_type* errorAnalyzer = nullptr;
 };
 
 }  // namespace souffle::ast::analysis

src/ast/analysis/ConstraintSystem.h

@@ -16,6 +16,7 @@
 
 #pragma once
 
+#include "ValueChecker.h"
 #include "souffle/utility/StreamUtil.h"
 #include <iostream>
 #include <map>
@@ -64,6 +65,13 @@ struct default_meet_op {
         return res;
     }
 };
+
+template <typename T>
+struct default_is_valid_op {
+    bool operator()(const T&) {
+        return true;
+    }
+};
 }  // namespace detail
 
 /**
@@ -85,11 +93,13 @@ struct default_meet_op {
  */
 template <typename T, typename meet_assign_op,
         typename bottom_factory = typename detail::default_bottom_factory<T>,
-        typename meet_op = typename detail::default_meet_op<T, meet_assign_op>>
+        typename meet_op = typename detail::default_meet_op<T, meet_assign_op>,
+        typename is_valid_op = typename detail::default_is_valid_op<T>>
 struct property_space {
     using value_type = T;
     using meet_assign_op_type = meet_assign_op;
     using meet_op_type = meet_op;
+    using is_valid_op_type = is_valid_op;
     using bottom_factory_type = bottom_factory;
 };
 
@@ -204,6 +214,10 @@ class Constraint {
         c.print(out);
         return out;
     }
+
+    virtual std::optional<std::string> customMessage() const {
+        return std::nullopt;
+    }
 };
 
 //----------------------------------------------------------------------
@@ -363,11 +377,18 @@ class Assignment {
  * @tparam Var the domain of variables handled by this problem
  */
 template <typename Var>
-class Problem {
+class Problem : public ValueChecker<Var> {
     // a few type definitions
     using constraint = Constraint<Var>;
     using constraint_ptr = std::shared_ptr<constraint>;
 
+    using value_type = typename Var::property_space::value_type;
+    using problem_type = Problem<Var>;
+
+public:
+    using unsat_core_type = typename std::set<constraint_ptr>;
+
+private:
     /** The list of covered constraints */
     std::vector<constraint_ptr> constraints;
 
@@ -409,6 +430,31 @@ class Problem {
         return assignment;
     }
 
+    unsat_core_type extractUnsatCore(const Var& var) {
+        unsat_core_type unsat_core;
+        const auto& constraints = (static_cast<Problem*>(this))->constraints;
+
+        while (true) {
+            Assignment<Var> assignment;
+            for (const auto& constraint : unsat_core) {
+                constraint->update(assignment);
+            }
+            if (!this->valueIsValid(assignment[var])) {
+                break;
+            }
+            auto size_unsat_core = unsat_core.size();
+            for (const auto& constraint : constraints) {
+                constraint->update(assignment);
+                if (!this->valueIsValid(assignment[var])) {
+                    unsat_core.insert(constraint);
+                    break;
+                }
+            }
+            if (size_unsat_core == unsat_core.size()) break;
+        }
+        return unsat_core;
+    }
+
     /** Enables a problem to be printed (debugging) */
     void print(std::ostream& out) const {
         if (constraints.empty()) {

src/ast/analysis/ErrorAnalyzer.h

@@ -0,0 +1,134 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2023, The Souffle Developers. All rights reserved.
+ * Licensed under the Universal Permissive License v 1.0 as shown at:
+ * - https://opensource.org/licenses/UPL
+ * - <souffle root>/licenses/SOUFFLE-UPL.txt
+ */
+
+/************************************************************************
+ *
+ * @file ErrorAnalyzer.h
+ *
+ * Extract reasons why something went wrong.
+ *
+ ***********************************************************************/
+
+#pragma once
+
+#include <functional>
+#include <map>
+#include <memory>
+#include <ostream>
+#include <set>
+#include <sstream>
+#include <vector>
+
+#include "ConstraintSystem.h"
+#include "ast/Argument.h"
+#include "parser/SrcLocation.h"
+#include "reports/ErrorReport.h"
+
+namespace souffle::ast::analysis {
+
+template <typename Var>
+class ErrorAnalyzer {
+private:
+    // A custom less functor to have the same result depending on the run and the platform
+    template <typename T>
+    struct less {
+        bool operator()(const std::shared_ptr<T>& lhs, const std::shared_ptr<T>& rhs) const {
+            return std::less<std::string>{}(str(lhs), str(rhs));
+        }
+        std::string str(const std::shared_ptr<T>& v) const {
+            std::stringstream ss;
+            ss << *v;
+            return ss.str();
+        }
+    };
+
+public:
+    using constraint_type = Constraint<Var>;
+    using constraint_ptr_type = std::shared_ptr<constraint_type>;
+    using unsat_core_type = typename std::set<constraint_ptr_type>;
+    using internal_unsat_core_type = typename std::set<constraint_ptr_type, less<constraint_type>>;
+
+    void addUnsatCore(const Argument* arg, const unsat_core_type& unsat_core) {
+        unsatCores[arg].insert(unsat_core.begin(), unsat_core.end());
+    }
+
+    void print(std::ostream& os) const {
+        for (const auto& [var, unsat_core] : unsatCores) {
+            os << var << " -- " << *var << "(";
+            for (const auto& constraint : unsat_core) {
+                os << *constraint << ", ";
+            }
+            os << ")\n";
+        }
+    }
+
+    void localizeConstraint(constraint_ptr_type constraint, const SrcLocation& loc) {
+        constraintLocations[constraint] = loc;
+    }
+
+    void addEquivalentArgumentSet(std::set<const Argument*> equivalentSet) {
+        for (const auto argument1 : equivalentSet) {
+            for (const auto argument2 : equivalentSet) {
+                if (argument1 == argument2) continue;
+                equivalentArguments.emplace(argument1, argument2);
+            }
+        }
+    }
+
+    void markArgumentAsExplained(const Argument* argument) {
+        explainedArguments.emplace(argument);
+        auto range = equivalentArguments.equal_range(argument);
+        for (auto it = range.first; it != range.second; ++it) {
+            explainedArguments.emplace(it->second);
+        }
+    }
+
+    bool argumentIsExplained(const Argument* argument) {
+        return explainedArguments.find(argument) != explainedArguments.end();
+    }
+
+    void explain(ErrorReport& report, const Argument* var, std::string message) {
+        if (argumentIsExplained(var)) return;
+        std::vector<DiagnosticMessage> additionalMessages;
+        bool doMarkAsExplained = true;
+        if (auto it = unsatCores.find(var); it != unsatCores.end()) {
+            if (!it->second.empty()) {
+                additionalMessages.emplace_back("Following constraints are incompatible:");
+                for (const auto& constraint : it->second) {
+                    std::stringstream ss;
+                    if (auto customMessage = constraint->customMessage(); customMessage) {
+                        ss << "   " << *customMessage;
+                    } else {
+                        ss << "   " << *constraint;
+                    }
+                    if (auto it = constraintLocations.find(constraint); it != constraintLocations.end()) {
+                        additionalMessages.emplace_back(ss.str(), it->second);
+                    } else {
+                        additionalMessages.emplace_back(ss.str());
+                    }
+                }
+            } else {
+                doMarkAsExplained = false;
+            }
+        }
+        Diagnostic diag{Diagnostic::Type::ERROR, DiagnosticMessage{message, var->getSrcLoc()},
+                std::move(additionalMessages)};
+        report.addDiagnostic(diag);
+        if (doMarkAsExplained) {
+            markArgumentAsExplained(var);
+        }
+    }
+
+private:
+    std::map<const Argument*, internal_unsat_core_type> unsatCores;
+    std::map<constraint_ptr_type, SrcLocation> constraintLocations;  // @todo maybe use pointer here
+    std::multimap<const Argument*, const Argument*> equivalentArguments;
+    std::set<const Argument*> explainedArguments;
+};
+
+}  // namespace souffle::ast::analysis

src/ast/analysis/ValueChecker.h

@@ -0,0 +1,33 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2023, The Souffle Developers. All rights reserved.
+ * Licensed under the Universal Permissive License v 1.0 as shown at:
+ * - https://opensource.org/licenses/UPL
+ * - <souffle root>/licenses/SOUFFLE-UPL.txt
+ */
+
+/************************************************************************
+ *
+ * @file ValueChecker.h
+ *
+ * Declares methods to check if value is valid.
+ *
+ ***********************************************************************/
+
+#pragma once
+
+namespace souffle::ast::analysis {
+
+template <typename Var>
+class ValueChecker {
+public:
+    using value_type = typename Var::property_space::value_type;
+    using is_valid_op_type = typename Var::property_space::is_valid_op_type;
+
+    virtual bool valueIsValid(const value_type& value) {
+        is_valid_op_type valid_op;
+        return valid_op(value);
+    }
+};
+
+}  // namespace souffle::ast::analysis