robustify the type-analysis debug report

The type-analysis debug report used to crash on various assertions because it assumed a well-typed program. However the first type-analysis runs before the semantics checker, hence the program may be ill-typed at that time. With this change the type-analysis debug report printer makes no assumptions about the expected types, instead it prints the infered types.
souffle-lang · Jun 20, 2024 · a1ab873 · a1ab873
1 parent 4de2942
commit a1ab873
Show file tree

Hide file tree

Showing 10 changed files with 67 additions and 102 deletions.
diff --git a/.github/workflows/CI-Tests.yml b/.github/workflows/CI-Tests.yml
@@ -67,7 +67,7 @@ jobs:
       if: ${{ matrix.domain == '32bit' }}
       uses: ./.github/actions/cmake-test
       with:
-        cmake-flags: -DSOUFFLE_CODE_COVERAGE=ON
+        cmake-flags: -DSOUFFLE_CODE_COVERAGE=ON -DSOUFFLE_TEST_DEBUG_REPORT
         n-chunks: ${{ needs.Test-Setup.outputs.n-chunks }}
         chunk: ${{ matrix.chunk }}
 

diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -104,6 +104,7 @@ option(SOUFFLE_CODE_COVERAGE "Enable coverage reporting" OFF)
 option(SOUFFLE_BASH_COMPLETION "Enable/Disable bash completion" OFF)
 option(SOUFFLE_USE_LIBFFI "Enable/Disable use of libffi" ON)
 option(SOUFFLE_CUSTOM_GETOPTLONG "Enable/Disable custom getopt_long implementation" OFF)
+option(SOUFFLE_TEST_DEBUG_REPORT "Enable/Disable generating debug-report for all tests" OFF)
 
 cmake_dependent_option(SOUFFLE_USE_LIBCPP "Link to libc++ instead of libstdc++" ON
     "CMAKE_CXX_COMPILER_ID STREQUAL Clang" OFF)

diff --git a/cmake/SouffleTests.cmake b/cmake/SouffleTests.cmake
@@ -159,9 +159,10 @@ function(SOUFFLE_RUN_TEST_HELPER)
 #and input paths
 #PARAM_FACTS_DIR_NAME - the name of the "facts" subdirectory in each test.
 #Usually just "facts" but can be different when running multi - tests
+#PARAM_DEBUG_REPORT - dump a debug report
     cmake_parse_arguments(
         PARAM
-        "COMPILED;COMPILED_SPLITTED;FUNCTORS;NEGATIVE;MULTI_TEST;NO_PREPROCESSOR;OUTPUT_STDOUT" # Options
+        "COMPILED;COMPILED_SPLITTED;FUNCTORS;NEGATIVE;MULTI_TEST;NO_PREPROCESSOR;OUTPUT_STDOUT;DEBUG_REPORT" # Options
         "TEST_NAME;CATEGORY;FACTS_DIR_NAME;EXTRA_DATA" #Single valued options
         "INCLUDE_DIRS" # Multi-valued options
         ${ARGV}
@@ -182,6 +183,10 @@ function(SOUFFLE_RUN_TEST_HELPER)
         set(SHORT_EXEC_STYLE "")
     endif()
 
+    if (PARAM_DEBUG_REPORT OR SOUFFLE_TEST_DEBUG_REPORT)
+      list(APPEND EXTRA_FLAGS "--debug-report=dbg.html")
+    endif()
+
     if (PARAM_NO_PREPROCESSOR)
       list(APPEND EXTRA_FLAGS "--no-preprocessor")
     else ()

diff --git a/src/ast/analysis/typesystem/Type.cpp b/src/ast/analysis/typesystem/Type.cpp
@@ -21,6 +21,7 @@
 #include "ast/Aggregator.h"
 #include "ast/Atom.h"
 #include "ast/BinaryConstraint.h"
+#include "ast/BooleanConstraint.h"
 #include "ast/BranchInit.h"
 #include "ast/Clause.h"
 #include "ast/IntrinsicAggregator.h"
@@ -557,11 +558,10 @@ void TypeAnalysis::run(const TranslationUnit& translationUnit) {
     this->translationUnit = &translationUnit;
 }
 
-void TypeAnnotationPrinter::branchOnArgument(const Argument* cur, const Type& type) {
+void TypeAnnotationPrinter::branchOnArgument(const Argument* cur) {
     if (isA<ast::Variable>(*cur)) {
-        auto var = as<ast::Variable>(cur);
-        auto inferedTypeName = argumentTypes.find(var)->second;
-        os << *as<ast::Variable>(cur) << "∈" << inferedTypeName;
+        auto inferedTypeName = argumentTypes.find(cur)->second;
+        os << *cur << "∈" << inferedTypeName;
     } else if (isA<UnnamedVariable>(*cur)) {
         os << "_";
     } else if (isA<NumericConstant>(*cur)) {
@@ -571,7 +571,7 @@ void TypeAnnotationPrinter::branchOnArgument(const Argument* cur, const Type& ty
     } else if (isA<NilConstant>(*cur)) {
         print_(type_identity<NilConstant>(), *as<NilConstant>(cur));
     } else if (isA<RecordInit>(*cur)) {
-        print_(type_identity<RecordInit>(), *as<RecordInit>(cur), *as<RecordType>(getBaseType(&type)));
+        print_(type_identity<RecordInit>(), *as<RecordInit>(cur));
     } else if (isA<BranchInit>(*cur)) {
         print_(type_identity<BranchInit>(), *as<BranchInit>(cur));
     } else if (isA<IntrinsicFunctor>(*cur)) {
@@ -595,18 +595,10 @@ void TypeAnnotationPrinter::print_(type_identity<Atom>, const Atom& atom) {
     auto name = atom.getQualifiedName();
     os << name << "(";
     auto args = atom.getArguments();
-    auto rel = program.getRelation(atom);
-    auto atts = rel->getAttributes();
 
     std::size_t i = 0;
     for (auto cur : args) {
-        const auto& declaredTypeName = atts[i]->getTypeName();
-        const auto& declaredType = typeEnv.getType(declaredTypeName);
-        assert(typeEnv.isType(declaredTypeName));
-        branchOnArgument(cur, declaredType);
-        if (isA<RecordInit>(cur) || isA<UnnamedVariable>(cur) || isA<TypeCast>(cur)) {
-            os << "∈{" << declaredTypeName << "}";
-        }
+        branchOnArgument(cur);
         if (i + 1 < args.size()) {
             os << ",";
         }
@@ -644,76 +636,52 @@ void TypeAnnotationPrinter::print_(type_identity<NumericConstant>, const Numeric
     }
 }
 
-void TypeAnnotationPrinter::print_(type_identity<BinaryConstraint>, const BinaryConstraint& rel) {
-    auto lhs = rel.getLHS();
-    auto lTySet = argumentTypes.find(lhs)->second;
-    assert(lTySet.size() == 1);
-    auto lTy = lTySet.begin();
-    branchOnArgument(lhs, *lTy);
-    if (isA<RecordInit>(lhs) || isA<UnnamedVariable>(lhs)) {
-        os << "∈{" << lTy->getName() << "}";
-    }
-
-    os << " " << rel.getBaseOperator() << " ";
+void TypeAnnotationPrinter::print_(type_identity<BinaryConstraint>, const BinaryConstraint& bin) {
+    auto lhs = bin.getLHS();
+    auto rhs = bin.getRHS();
+    branchOnArgument(lhs);
+    os << " " << bin.getBaseOperator() << " ";
+    branchOnArgument(rhs);
+}
 
-    auto rhs = rel.getRHS();
-    auto rTySet = argumentTypes.find(rhs)->second;
-    assert(rTySet.size() == 1);
-    auto rTy = rTySet.begin();
-    branchOnArgument(rhs, *rTy);
-    if (isA<RecordInit>(rhs) || isA<UnnamedVariable>(rhs)) {
-        os << "∈{" << rTy->getName() << "}";
-    }
+void TypeAnnotationPrinter::print_(type_identity<BooleanConstraint>, const BooleanConstraint& c) {
+    os << c;
 }
 
 void TypeAnnotationPrinter::print_(type_identity<IntrinsicFunctor>, const IntrinsicFunctor& fun) {
     auto arguments = fun.getArguments();
     if (arguments.size() == 2) {  // binary
-        auto tySet = argumentTypes.find(arguments[0])->second;
-        assert(tySet.size() == 1);
-        auto ty = tySet.begin();
         os << "(";
-        branchOnArgument(arguments[0], *ty);
-        if (isA<RecordInit>(arguments[0]) || isA<UnnamedVariable>(arguments[0])) {
-            os << "∈{" << ty->getName() << "}";
-        }
-
+        branchOnArgument(arguments[0]);
         os << " " << fun.getBaseFunctionOp() << " ";
-
-        auto tySet2 = argumentTypes.find(arguments[1])->second;
-        assert(tySet2.size() == 1);
-        auto ty2 = tySet2.begin();
-        branchOnArgument(arguments[1], *ty2);
-        if (isA<RecordInit>(arguments[1]) || isA<UnnamedVariable>(arguments[1])) {
-            os << "∈{" << ty2->getName() << "}";
-        }
-
+        branchOnArgument(arguments[1]);
         os << ")";
     } else {
         os << fun.getBaseFunctionOp() << "(";
         for (std::size_t i = 0; i < arguments.size(); ++i) {
-            TypeAttribute argType = typeAnalysis.getFunctorParamTypeAttribute(fun, i);
-            auto& ty = typeEnv.getConstantType(argType);
-            branchOnArgument(arguments[i], ty);
+            branchOnArgument(arguments[i]);
             if (i + 1 < arguments.size()) {
                 os << ",";
             }
         }
         os << ")";
     }
+    const TypeSet& ts = argumentTypes.at(&fun);
+    os << "∈" << ts;
 }
 
 void TypeAnnotationPrinter::print_(type_identity<UserDefinedFunctor>, const UserDefinedFunctor& fun) {
     auto arguments = fun.getArguments();
     os << "@" << fun.getName() << "(";
     for (std::size_t i = 0; i < arguments.size(); ++i) {
-        const auto& ty = typeAnalysis.getFunctorParamType(fun, i);
-        branchOnArgument(arguments[i], ty);
+        branchOnArgument(arguments[i]);
         if (i + 1 < arguments.size()) {
             os << ",";
         }
     }
     os << ")";
+    const TypeSet& ts = argumentTypes.at(&fun);
+    os << "∈" << ts;
 }
 
 void TypeAnnotationPrinter::print_(type_identity<Counter>, [[maybe_unused]] const Counter& counter) {
@@ -727,52 +695,39 @@ void TypeAnnotationPrinter::print_(
 
 void TypeAnnotationPrinter::print_(type_identity<TypeCast>, const ast::TypeCast& typeCast) {
     os << "as(";
-    auto& ty = typeEnv.getType(typeCast.getType());
-    branchOnArgument(typeCast.getValue(), ty);
-    os << "," << ty.getName() << ")";
+    branchOnArgument(typeCast.getValue());
+    os << "," << typeCast.getType() << ")";
+    const TypeSet& ts = argumentTypes.at(&typeCast);
+    os << "∈" << ts;
 }
 
-void TypeAnnotationPrinter::print_(
-        type_identity<RecordInit>, const RecordInit& record, const RecordType& type) {
+void TypeAnnotationPrinter::print_(type_identity<RecordInit>, const RecordInit& record) {
     auto arguments = record.getArguments();
-    const auto& ftypes = type.getFields();
     os << "[";
     for (std::size_t i = 0; i < arguments.size(); ++i) {
-        branchOnArgument(arguments[i], *ftypes[i]);
-        if (isA<RecordInit>(arguments[i]) || isA<UnnamedVariable>(arguments[i])) {
-            os << "∈{" << (*ftypes[i]).getName() << "}";
-        }
+        branchOnArgument(arguments[i]);
         if (i + 1 < arguments.size()) {
             os << ",";
         }
     }
     os << "]";
+    const TypeSet& ts = argumentTypes.at(&record);
+    os << "∈" << ts;
 }
 
 void TypeAnnotationPrinter::print_(type_identity<BranchInit>, const BranchInit& adt) {
-    auto* correspondingType = sumTypesBranches.getType(adt.getBranchName());
-
-    assert(correspondingType != nullptr);
-    assert(isA<AlgebraicDataType>(correspondingType));
-
-    auto branchTypes = as<AlgebraicDataType>(correspondingType)->getBranchTypes(adt.getBranchName());
     auto branchArgs = adt.getArguments();
 
-    assert(branchTypes.size() == branchArgs.size());
-
     os << "$" << adt.getBranchName() << "(";
     for (std::size_t i = 0; i < branchArgs.size(); i++) {
-        auto arg = branchArgs[i];
-        auto argTy = branchTypes[i];
-        branchOnArgument(arg, *argTy);
-        if (isA<RecordInit>(arg) || isA<UnnamedVariable>(arg)) {
-            os << "∈{" << argTy->getName() << "}";
-        }
+        branchOnArgument(branchArgs[i]);
         if (i + 1 < branchArgs.size()) {
             os << ", ";
         }
     }
     os << ")";
+    const TypeSet& ts = argumentTypes.at(&adt);
+    os << "∈" << ts;
 }
 
 void TypeAnnotationPrinter::print_(type_identity<Aggregator>, const Aggregator& agg) {
@@ -781,14 +736,13 @@ void TypeAnnotationPrinter::print_(type_identity<Aggregator>, const Aggregator&
     os << baseOperator << " ";
     auto targetExpr = agg.getTargetExpression();
     if (targetExpr /* the target expression can be null */) {
-        auto tySet = argumentTypes.find(targetExpr)->second;
-        assert(tySet.size() == 1);
-        auto ty = tySet.begin();
-        branchOnArgument(targetExpr, *ty);
+        branchOnArgument(targetExpr);
     }
     os << " : { ";
     printBodyLiterals(bodyLiterals, "        ");
     os << " }";
+    const TypeSet& ts = argumentTypes.at(&agg);
+    os << "∈" << ts;
 }
 
 void TypeAnnotationPrinter::printBodyLiterals(std::vector<Literal*> bodyLiterals, const std::string& spc) {
@@ -800,6 +754,8 @@ void TypeAnnotationPrinter::printBodyLiterals(std::vector<Literal*> bodyLiterals
             print_(type_identity<Negation>(), *as<Negation>(*cur));
         } else if (isA<BinaryConstraint>(*cur)) {
             print_(type_identity<BinaryConstraint>(), *as<BinaryConstraint>(*cur));
+        } else if (isA<BooleanConstraint>(*cur)) {
+            print_(type_identity<BooleanConstraint>(), *as<BooleanConstraint>(*cur));
         } else {
             os << "(?)";
         }

diff --git a/src/ast/analysis/typesystem/Type.h b/src/ast/analysis/typesystem/Type.h
@@ -18,6 +18,7 @@
 
 #include "AggregateOp.h"
 #include "FunctorOps.h"
+#include "ast/BooleanConstraint.h"
 #include "ast/Clause.h"
 #include "ast/NumericConstant.h"
 #include "ast/TranslationUnit.h"
@@ -163,7 +164,7 @@ class TypeAnalysis : public Analysis {
  */
 class TypeAnnotationPrinter {
 public:
-    TypeAnnotationPrinter(const TranslationUnit* tu, const std::map<const Argument*, TypeSet> argumentTypes,
+    TypeAnnotationPrinter(const TranslationUnit* tu, const std::map<const Argument*, TypeSet>& argumentTypes,
             std::ostream& os)
             : tu(tu), argumentTypes(argumentTypes), os(os) {}
 
@@ -177,24 +178,25 @@ class TypeAnnotationPrinter {
     const SumTypeBranchesAnalysis& sumTypesBranches = tu->getAnalysis<SumTypeBranchesAnalysis>();
     const TypeAnalysis& typeAnalysis = tu->getAnalysis<TypeAnalysis>();
 
-    std::map<const Argument*, TypeSet> argumentTypes;
+    const std::map<const Argument*, TypeSet>& argumentTypes;
     std::ostream& os;
 
-    void branchOnArgument(const Argument*, const Type&);
+    void branchOnArgument(const Argument*);
     void print_(type_identity<Atom>, const Atom& atom);
     void print_(type_identity<Negation>, const Negation& cur);
     void print_(type_identity<StringConstant>, const StringConstant& cnst);
     void print_(type_identity<NumericConstant>, const NumericConstant& constant);
     void print_(type_identity<NilConstant>, const NilConstant& constant);
-    void print_(type_identity<BinaryConstraint>, const BinaryConstraint& rel);
+    void print_(type_identity<BinaryConstraint>, const BinaryConstraint& bin);
     void print_(type_identity<IntrinsicFunctor>, const IntrinsicFunctor& fun);
     void print_(type_identity<UserDefinedFunctor>, const UserDefinedFunctor& fun);
     void print_(type_identity<Counter>, const Counter& counter);
     void print_(type_identity<IterationCounter>, const IterationCounter& counter);
     void print_(type_identity<TypeCast>, const ast::TypeCast& typeCast);
-    void print_(type_identity<RecordInit>, const RecordInit& record, const RecordType&);
+    void print_(type_identity<RecordInit>, const RecordInit& record);
     void print_(type_identity<BranchInit>, const BranchInit& adt);
     void print_(type_identity<Aggregator>, const Aggregator& agg);
+    void print_(type_identity<BooleanConstraint>, const BooleanConstraint& c);
     void printBodyLiterals(std::vector<Literal*> literals, const std::string& spc);
 };
 

diff --git a/src/ast/analysis/typesystem/TypeSystem.h b/src/ast/analysis/typesystem/TypeSystem.h
@@ -364,12 +364,12 @@ class AlgebraicDataType : public Type {
                 [](const Branch& left, const Branch& right) { return left.name.lexicalLess(right.name); });
     }
 
-    const std::vector<const Type*>& getBranchTypes(const QualifiedName& name) const {
+    std::vector<const Type*> getBranchTypes(const QualifiedName& name) const {
         for (auto& branch : branches) {
             if (branch.name == name) return branch.types;
         }
         // Branch doesn't exist.
-        throw std::out_of_range("Trying to access non-existing branch.");
+        return {};
     }
 
     /** Return the branches as a sorted vector */
@@ -523,7 +523,9 @@ struct TypeSet {
     /** Print type set */
     void print(std::ostream& out) const {
         if (all) {
-            out << "{ - all types - }";
+            out << "⊤";
+        } else if (types.empty()) {
+            out << "∅";
         } else {
             out << "{"
                 << join(types, ",", [](std::ostream& out, const Type* type) { out << type->getName(); })

diff --git a/src/ast/transform/TypeChecker.cpp b/src/ast/transform/TypeChecker.cpp
@@ -495,7 +495,7 @@ void TypeCheckerImpl::visit_(type_identity<BranchInit>, const BranchInit& adt) {
     // We know now that the set "types" is a singleton
     auto& sumType = *as<analysis::AlgebraicDataType>(*types.begin());
 
-    auto& argsDeclaredTypes = sumType.getBranchTypes(adt.getBranchName());
+    auto argsDeclaredTypes = sumType.getBranchTypes(adt.getBranchName());
 
     auto args = adt.getArguments();
 

diff --git a/tests/evaluation/CMakeLists.txt b/tests/evaluation/CMakeLists.txt
@@ -26,7 +26,7 @@ positive_test(aggregates_nested)
 positive_test(aggregates_non_materialised)
 positive_test(aggregates7)
 positive_test(aggregate_witnesses)
-positive_test(aliases)
+positive_test(aliases DEBUG_REPORT)
 positive_test(arithm)
 positive_test(average)
 positive_test(bad_regex)

diff --git a/tests/example/euclid/euclid.dl b/tests/example/euclid/euclid.dl
@@ -70,9 +70,11 @@ Simplify([head,tail],[newHead,newTail]) :-
 // Helper method for simplify
 ToGcdInt(numerator,denominator) :-
     ToSimplify([head,tail]),
-    Simplify(tail,newTail),
     head = [numerator,denominator] ,
-    (newTail != nil; numerator != 0).
+    ( Simplify(tail, newTail),
+      newTail != nil
+    ; numerator != 0
+    ).
 
 // -- Add polynomials recursively -- //
 

diff --git a/tests/example/euclid/euclid.err b/tests/example/euclid/euclid.err
@@ -1,12 +1,9 @@
 Warning: Variable denominator only occurs once in file euclid.dl at line 61
     head = [0,denominator].
 --------------^-------------
-Warning: Variable newTail only occurs once in file euclid.dl at line 73
-    Simplify(tail,newTail),
-------------------^---------
-Warning: Variable denominator only occurs once in file euclid.dl at line 128
+Warning: Variable denominator only occurs once in file euclid.dl at line 130
     head = [0,denominator].
 --------------^-------------
-Warning: Variable denominator only occurs once in file euclid.dl at line 132
+Warning: Variable denominator only occurs once in file euclid.dl at line 134
     head = [numerator,denominator], numerator!=0.
 ----------------------^---------------------------