souffle::ast::transform::SemanticCheckerImpl Struct Reference

Collaboration diagram for souffle::ast::transform::SemanticCheckerImpl:

Public Member Functions
	SemanticCheckerImpl (TranslationUnit &tu)

Data Fields
TranslationUnit &	tu

Private Member Functions
void	checkAggregator (const Aggregator &aggregator)
void	checkArgument (const Argument &arg)
void	checkAtom (const Atom &atom)
void	checkBranchInits ()
	check if all the branches refer to the existing types. More...
void	checkClause (const Clause &clause)
void	checkComplexRule (std::set< const Clause * > multiRule)
void	checkConstant (const Argument &argument)
void	checkFact (const Clause &fact)
void	checkInlining ()
void	checkIO ()
void	checkLiteral (const Literal &literal)
void	checkNamespaces ()
void	checkRelation (const Relation &relation)
void	checkRelationDeclaration (const Relation &relation)
void	checkWitnessProblem ()
bool	isDependent (const Clause &agg1, const Clause &agg2)
	agg1, agg2 are clauses which contain no head, and consist of a single literal that contains an aggregate. More...

Private Attributes
const IOTypeAnalysis &	ioTypes = *tu.getAnalysis<IOTypeAnalysis>()
const PrecedenceGraphAnalysis &	precedenceGraph = *tu.getAnalysis<PrecedenceGraphAnalysis>()
const Program &	program = tu.getProgram()
const RecursiveClausesAnalysis &	recursiveClauses = *tu.getAnalysis<RecursiveClausesAnalysis>()
ErrorReport &	report = tu.getErrorReport()
const SCCGraphAnalysis &	sccGraph = *tu.getAnalysis<SCCGraphAnalysis>()
const SumTypeBranchesAnalysis &	sumTypesBranches = *tu.getAnalysis<SumTypeBranchesAnalysis>()
const TypeEnvironment &	typeEnv = tu.getAnalysis<TypeEnvironmentAnalysis>()->getTypeEnvironment()

Detailed Description

Definition at line 108 of file SemanticChecker.cpp.

Constructor & Destructor Documentation

SemanticCheckerImpl()

souffle::ast::transform::SemanticCheckerImpl::SemanticCheckerImpl

(

TranslationUnit &

tu

)

Definition at line 149 of file SemanticChecker.cpp.

                                           {
            // mute all relations
            for (Relation* rel : program.getRelations()) {
                rel->addQualifier(RelationQualifier::SUPPRESSED);
            }
        } else {
            // mute only the given relations (if they exist)
            for (auto& relname : suppressedRelations) {
                const std::vector<std::string> comps = splitString(relname, '.');
                if (!comps.empty()) {
                    // generate the relation identifier
                    QualifiedName relid(comps[0]);
                    for (size_t i = 1; i < comps.size(); i++) {
                        relid.append(comps[i]);
                    }
 
                    // update suppressed qualifier if the relation is found
                    if (Relation* rel = getRelation(program, relid)) {
                        rel->addQualifier(RelationQualifier::SUPPRESSED);
                    }
                }
            }
        }
    }
 
    checkBranchInits();
 
    // check rules
    for (auto* rel : program.getRelations()) {
        checkRelation(*rel);
    }
    for (auto* clause : program.getClauses()) {
        checkClause(*clause);
    }
 
    // Group clauses that stem from a single complex rule
    // with multiple headers/disjunction etc. The grouping
    // is performed via their source-location.
    std::map<SrcLocation, std::set<const Clause*>> multiRuleMap;
    for (auto* clause : program.getClauses()) {
        // collect clauses of a multi rule, i.e., they have the same source locator
        multiRuleMap[clause->getSrcLoc()].insert(clause);
    }
 
    // check complex rule
    for (const auto& multiRule : multiRuleMap) {
        checkComplexRule(multiRule.second);
    }
 
    checkNamespaces();
    checkIO();
    checkWitnessProblem();
    checkInlining();
 
    // Run grounded terms checker
    GroundedTermsChecker().verify(tu);
 
    // Check types
    TypeChecker().verify(tu);
 
    // - stratification --
    // check for cyclic dependencies
    for (Relation* cur : program.getRelations()) {
        size_t scc = sccGraph.getSCC(cur);
        if (sccGraph.isRecursive(scc)) {
            for (const Relation* cyclicRelation : sccGraph.getInternalRelations(scc)) {
                // Negations and aggregations need to be stratified
                const Literal* foundLiteral = nullptr;
                bool hasNegation = hasClauseWithNegatedRelation(cyclicRelation, cur, &program, foundLiteral);
                if (hasNegation ||
                        hasClauseWithAggregatedRelation(cyclicRelation, cur, &program, foundLiteral)) {
                    auto const& relSet = sccGraph.getInternalRelations(scc);
                    std::set<const Relation*, NameComparison> sortedRelSet(relSet.begin(), relSet.end());
                    // Negations and aggregations need to be stratified
                    std::string relationsListStr = toString(join(sortedRelSet, ",",
                            [](std::ostream& out, const Relation* r) { out << r->getQualifiedName(); }));
                    std::vector<DiagnosticMessage> messages;
                    messages.push_back(DiagnosticMessage(
                            "Relation " + toString(cur->getQualifiedName()), cur->getSrcLoc()));
                    std::string negOrAgg = hasNegation ? "negation" : "aggregation";
                    messages.push_back(
                            DiagnosticMessage("has cyclic " + negOrAgg, foundLiteral->getSrcLoc()));
                    report.addDiagnostic(Diagnostic(Diagnostic::Type::ERROR,
                            DiagnosticMessage("Unable to stratify relation(s) {" + relationsListStr + "}"),
                            messages));
                    break;
                }
            }
        }
    }
}
 
void SemanticCheckerImpl::checkAtom(const Atom& atom) {
    // check existence of relation
    auto* r = getRelation(program, atom.getQualifiedName());
    if (r == nullptr) {
        report.addError("Undefined relation " + toString(atom.getQualifiedName()), atom.getSrcLoc());

References souffle::ast::Program::getRelations(), program, rel(), and souffle::SUPPRESSED.

Here is the call graph for this function:

Member Function Documentation

checkAggregator()

void souffle::ast::transform::SemanticCheckerImpl::checkAggregator ( const Aggregator &  aggregator )

private

Definition at line 375 of file SemanticChecker.cpp.

                                                                                 {
            if (candidateAggregate != aggregator) {
                return;
            }
            // Get the literal containing the aggregator and put it into a dummy clause
            // so we can get information about groundedness
            dummyClauseAggregator.addToBody(souffle::clone(&parentLiteral));
        });
    });
 
    visitDepthFirst(program, [&](const Literal& parentLiteral) {
        visitDepthFirst(parentLiteral, [&](const Aggregator& /* otherAggregate */) {
            // Create the other aggregate's dummy clause
            Clause dummyClauseOther;
            dummyClauseOther.addToBody(souffle::clone(&parentLiteral));
            // Check dependency between the aggregator and this one
            if (isDependent(dummyClauseAggregator, dummyClauseOther) &&
                    isDependent(dummyClauseOther, dummyClauseAggregator)) {
                report.addError("Mutually dependent aggregate", aggregator.getSrcLoc());
            }
        });
    });
 
    for (Literal* literal : aggregator.getBodyLiterals()) {
        checkLiteral(*literal);
    }
}
 
void SemanticCheckerImpl::checkArgument(const Argument& arg) {
    if (const auto* agg = dynamic_cast<const Aggregator*>(&arg)) {
        checkAggregator(*agg);
    } else if (const auto* func = dynamic_cast<const Functor*>(&arg)) {
        for (auto arg : func->getArguments()) {

References souffle::clone().

Here is the call graph for this function:

checkArgument()

void souffle::ast::transform::SemanticCheckerImpl::checkArgument ( const Argument &  arg )

private

Definition at line 409 of file SemanticChecker.cpp.

          {
 
/**
 * Check if the argument can be statically evaluated
 * and thus in particular, if it should be allowed to appear as argument in facts.

checkAtom()

void souffle::ast::transform::SemanticCheckerImpl::checkAtom ( const Atom &  atom )

private

Definition at line 248 of file SemanticChecker.cpp.

                                          {
        report.addError(
                "Mismatching arity of relation " + toString(atom.getQualifiedName()), atom.getSrcLoc());
    }
 
    for (const Argument* arg : atom.getArguments()) {
        checkArgument(*arg);
    }
}
 
void SemanticCheckerImpl::checkBranchInits() {
    visitDepthFirst(program.getClauses(), [&](const BranchInit& adt) {
        auto* type = sumTypesBranches.getType(adt.getConstructor());
        if (type == nullptr) {
            report.addError("Undeclared branch", adt.getSrcLoc());

checkBranchInits()

void souffle::ast::transform::SemanticCheckerImpl::checkBranchInits ( )

private

check if all the branches refer to the existing types.

Definition at line 266 of file SemanticChecker.cpp.

                                          {
            report.addError(tfm::format("Invalid arity, the declared arity of %s is %s", adt.getConstructor(),
                                    declaredArity),
                    adt.getSrcLoc());
            return;
        }
    });
}
 
namespace {
 
/**
 * Get unnamed variables except those that appear inside aggregates.
 */

References souffle::ErrorReport::addError(), tinyformat::format(), and report.

Here is the call graph for this function:

checkClause()

void souffle::ast::transform::SemanticCheckerImpl::checkClause ( const Clause &  clause )

private

Definition at line 470 of file SemanticChecker.cpp.

                      : clause.getBodyLiterals()) {
        checkLiteral(*lit);
    }
 
    // check facts
    if (isFact(clause)) {
        checkFact(clause);
    }
 
    // check whether named unnamed variables of the form _<ident>
    // are only used once in a clause; if not, warnings will be
    // issued.
    std::map<std::string, int> var_count;
    std::map<std::string, const ast::Variable*> var_pos;
    visitDepthFirst(clause, [&](const ast::Variable& var) {
        var_count[var.getName()]++;
        var_pos[var.getName()] = &var;
    });
    for (const auto& cur : var_count) {
        int numAppearances = cur.second;
        const auto& varName = cur.first;
        const auto& varLocation = var_pos[varName]->getSrcLoc();
        if (varName[0] == '_') {
            assert(varName.size() > 1 && "named variable should not be a single underscore");
            if (numAppearances > 1) {
                report.addWarning("Variable " + varName + " marked as singleton but occurs more than once",
                        varLocation);
            }
        }
    }
 
    // check execution plan
    if (clause.getExecutionPlan() != nullptr) {
        auto numAtoms = getBodyLiterals<Atom>(clause).size();
        for (const auto& cur : clause.getExecutionPlan()->getOrders()) {
            bool isComplete = true;
            auto order = cur.second->getOrder();
            for (unsigned i = 1; i <= order.size(); i++) {
                if (!contains(order, i)) {
                    isComplete = false;
                    break;
                }
            }
            if (order.size() != numAtoms || !isComplete) {
                report.addError("Invalid execution order in plan", cur.second->getSrcLoc());
            }
        }
    }
 
    // check auto-increment
    if (recursiveClauses.recursive(&clause)) {
        visitDepthFirst(clause, [&](const Counter& ctr) {
            report.addError("Auto-increment functor in a recursive rule", ctr.getSrcLoc());
        });
    }
}
 
void SemanticCheckerImpl::checkComplexRule(std::set<const Clause*> multiRule) {
    std::map<std::string, int> var_count;
    std::map<std::string, const ast::Variable*> var_pos;
 
    // Count the variable occurrence for the body of a

checkComplexRule()

void souffle::ast::transform::SemanticCheckerImpl::checkComplexRule ( std::set< const Clause * >  multiRule )

private

Definition at line 537 of file SemanticChecker.cpp.

                      : (*multiRule.begin())->getBodyLiterals()) {
        visitDepthFirst(*literal, [&](const ast::Variable& var) {
            var_count[var.getName()]++;
            var_pos[var.getName()] = &var;
        });
    }
 
    // Count variable occurrence for each head separately
    for (auto clause : multiRule) {
        visitDepthFirst(*(clause->getHead()), [&](const ast::Variable& var) {
            var_count[var.getName()]++;
            var_pos[var.getName()] = &var;
        });
    }
 
    // Check that a variables occurs more than once
    for (const auto& cur : var_count) {
        int numAppearances = cur.second;
        const auto& varName = cur.first;
        const auto& varLocation = var_pos[varName]->getSrcLoc();
        if (varName[0] != '_' && numAppearances == 1) {
            report.addWarning("Variable " + varName + " only occurs once", varLocation);
        }
    }
}
 
void SemanticCheckerImpl::checkRelationDeclaration(const Relation& relation) {
    const auto& attributes = relation.getAttributes();
    assert(attributes.size() == relation.getArity() && "mismatching attribute size and arity");
 
    for (size_t i = 0; i < relation.getArity(); i++) {

References souffle::ast::visitDepthFirst().

Here is the call graph for this function:

checkConstant()

void souffle::ast::transform::SemanticCheckerImpl::checkConstant ( const Argument &  argument )

private

checkFact()

void souffle::ast::transform::SemanticCheckerImpl::checkFact ( const Clause &  fact )

private

Definition at line 449 of file SemanticChecker.cpp.

                        {
        return;  // checked by clause
    }
 
    // facts must only contain constants
    for (auto* arg : head->getArguments()) {
        if (!isConstantArgument(arg)) {
            report.addError("Argument in fact is not constant", arg->getSrcLoc());
        }
    }
}
 
void SemanticCheckerImpl::checkClause(const Clause& clause) {
    // check head atom
    checkAtom(*clause.getHead());
 
    // Check for absence of underscores in head

checkInlining()

void souffle::ast::transform::SemanticCheckerImpl::checkInlining ( )

private

Definition at line 791 of file SemanticChecker.cpp.

                                {
            inlinedRelations.insert(relation);
            if (ioTypes.isIO(relation)) {
                report.addError(
                        "IO relation " + toString(relation->getQualifiedName()) + " cannot be inlined",
                        relation->getSrcLoc());
            }
        }
    }
 
    // Check 1:
    // Let G' be the subgraph of the precedence graph G containing only those nodes
    // which are marked with the inline directive.
    // If G' contains a cycle, then inlining cannot be performed.
 
    RelationSet unvisited;  // nodes that have not been visited yet
    RelationSet visiting;   // nodes that we are currently visiting
    RelationSet visited;    // nodes that have been completely explored
 
    // All nodes are initially unvisited
    for (const Relation* rel : inlinedRelations) {
        unvisited.insert(rel);
    }
 
    // Remember the parent node of each visited node to construct the found cycle
    std::map<const Relation*, const Relation*> origins;
 
    std::vector<QualifiedName> result =
            findInlineCycle(precedenceGraph, origins, nullptr, unvisited, visiting, visited);
 
    // If the result contains anything, then a cycle was found
    if (!result.empty()) {
        Relation* cycleOrigin = getRelation(program, result[result.size() - 1]);
 
        // Construct the string representation of the cycle
        std::stringstream cycle;
        cycle << "{" << cycleOrigin->getQualifiedName();
 
        // Print it backwards to preserve the initial cycle order
        for (int i = result.size() - 2; i >= 0; i--) {
            cycle << ", " << result[i];
        }
 
        cycle << "}";
 
        report.addError(
                "Cannot inline cyclically dependent relations " + cycle.str(), cycleOrigin->getSrcLoc());
    }
 
    // Check 2:
    // Cannot use the counter argument ('$') in inlined relations
 
    // Check if an inlined literal ever takes in a $
    visitDepthFirst(program, [&](const Atom& atom) {
        Relation* associatedRelation = getRelation(program, atom.getQualifiedName());
        if (associatedRelation != nullptr && isInline(associatedRelation)) {
            visitDepthFirst(atom, [&](const Argument& arg) {
                if (isA<Counter>(&arg)) {
                    report.addError(
                            "Cannot inline literal containing a counter argument '$'", arg.getSrcLoc());
                }
            });
        }
    });
 
    // Check if an inlined clause ever contains a $
    for (const Relation* rel : inlinedRelations) {
        for (Clause* clause : getClauses(program, *rel)) {
            visitDepthFirst(*clause, [&](const Argument& arg) {
                if (isA<Counter>(&arg)) {
                    report.addError(
                            "Cannot inline clause containing a counter argument '$'", arg.getSrcLoc());
                }
            });
        }
    }
 
    // Check 3:
    // Suppose the relation b is marked with the inline directive, but appears negated
    // in a clause. Then, if b introduces a new variable in its body, we cannot inline
    // the relation b.
 
    // Find all relations with the inline declarative that introduce new variables in their bodies
    RelationSet nonNegatableRelations;
    for (const Relation* rel : inlinedRelations) {
        bool foundNonNegatable = false;
        for (const Clause* clause : getClauses(program, *rel)) {
            // Get the variables in the head
            std::set<std::string> headVariables;
            visitDepthFirst(*clause->getHead(),
                    [&](const ast::Variable& var) { headVariables.insert(var.getName()); });
 
            // Get the variables in the body
            std::set<std::string> bodyVariables;
            visitDepthFirst(clause->getBodyLiterals(),
                    [&](const ast::Variable& var) { bodyVariables.insert(var.getName()); });
 
            // Check if all body variables are in the head
            // Do this separately to the above so only one error is printed per variable
            for (const std::string& var : bodyVariables) {
                if (headVariables.find(var) == headVariables.end()) {
                    nonNegatableRelations.insert(rel);
                    foundNonNegatable = true;
                    break;
                }
            }
 
            if (foundNonNegatable) {
                break;
            }
        }
    }
 
    // Check that these relations never appear negated
    visitDepthFirst(program, [&](const Negation& neg) {
        Relation* associatedRelation = getRelation(program, neg.getAtom()->getQualifiedName());
        if (associatedRelation != nullptr &&
                nonNegatableRelations.find(associatedRelation) != nonNegatableRelations.end()) {
            report.addError(
                    "Cannot inline negated relation which may introduce new variables", neg.getSrcLoc());
        }
    });
 
    // Check 4:
    // Don't support inlining atoms within aggregators at this point.
 
    // Reasoning: Suppose we have an aggregator like `max X: a(X)`, where `a` is inlined to `a1` and `a2`.
    // Then, `max X: a(X)` will become `max( max X: a1(X),  max X: a2(X) )`. Suppose further that a(X) has
    // values X where it is true, while a2(X) does not. Then, the produced argument
    // `max( max X: a1(X),  max X: a2(X) )` will not return anything (as one of its arguments fails), while
    // `max X: a(X)` will.
    // Can work around this with emptiness checks (e.g. `!a1(_), ... ; !a2(_), ... ; ...`)
 
    // This corner case prevents generalising aggregator inlining with the current set up.
 
    visitDepthFirst(program, [&](const Aggregator& aggr) {
        visitDepthFirst(aggr, [&](const Atom& subatom) {
            const Relation* rel = getRelation(program, subatom.getQualifiedName());
            if (rel != nullptr && isInline(rel)) {
                report.addError("Cannot inline relations that appear in aggregator", subatom.getSrcLoc());
            }
        });
    });
 
    // Check 5:
    // Suppose a relation `a` is inlined, appears negated in a clause, and contains a
    // (possibly nested) unnamed variable in its arguments. Then, the atom can't be
    // inlined, as unnamed variables are named during inlining (since they may appear
    // multiple times in an inlined-clause's body) => ungroundedness!
 
    // Exception: It's fine if the unnamed variable appears in a nested aggregator, as
    // the entire aggregator will automatically be grounded.
 
    // TODO (azreika): special case where all rules defined for `a` use the
    // underscored-argument exactly once: can workaround by remapping the variable
    // back to an underscore - involves changes to the actual inlining algo, though
 
    // Returns the pair (isValid, lastSrcLoc) where:
    //  - isValid is true if and only if the node contains an invalid underscore, and
    //  - lastSrcLoc is the source location of the last visited node
    std::function<std::pair<bool, SrcLocation>(const Node*)> checkInvalidUnderscore = [&](const Node* node) {
        if (isA<UnnamedVariable>(node)) {
            // Found an invalid underscore
            return std::make_pair(true, node->getSrcLoc());
        } else if (isA<Aggregator>(node)) {
            // Don't care about underscores within aggregators
            return std::make_pair(false, node->getSrcLoc());
        }
 
        // Check if any children nodes use invalid underscores
        for (const Node* child : node->getChildNodes()) {
            std::pair<bool, SrcLocation> childStatus = checkInvalidUnderscore(child);
            if (childStatus.first) {
                // Found an invalid underscore
                return childStatus;
            }
        }
 
        return std::make_pair(false, node->getSrcLoc());
    };
 
    // Perform the check
    visitDepthFirst(program, [&](const Negation& negation) {
        const Atom* associatedAtom = negation.getAtom();
        const Relation* associatedRelation = getRelation(program, associatedAtom->getQualifiedName());
        if (associatedRelation != nullptr && isInline(associatedRelation)) {
            std::pair<bool, SrcLocation> atomStatus = checkInvalidUnderscore(associatedAtom);
            if (atomStatus.first) {
                report.addError(
                        "Cannot inline negated atom containing an unnamed variable unless the variable is "
                        "within an aggregator",
                        atomStatus.second);
            }
        }
    });
}
 
// Check that type and relation names are disjoint sets.
void SemanticCheckerImpl::checkNamespaces() {
    std::map<std::string, SrcLocation> names;
 
    // Find all names and report redeclarations as we go.

References souffle::ErrorReport::addError(), relation, and souffle::toString().

Here is the call graph for this function:

checkIO()

void souffle::ast::transform::SemanticCheckerImpl::checkIO ( )

private

Definition at line 623 of file SemanticChecker.cpp.

                               : program.getDirectives()) {
        checkIO(directive);
    }
}
 
/**
 *  A witness is considered "invalid" if it is trying to export a witness
 *  out of a count, sum, or mean aggregate.
 *
 *  However we need to be careful: Sometimes a witness variables occurs within the body

checkLiteral()

void souffle::ast::transform::SemanticCheckerImpl::checkLiteral ( const Literal &  literal )

private

Definition at line 309 of file SemanticChecker.cpp.

                                                 {
        checkAtom(*neg->getAtom());
    }
 
    if (const auto* constraint = as<BinaryConstraint>(literal)) {
        checkArgument(*constraint->getLHS());
        checkArgument(*constraint->getRHS());
 
        std::set<const UnnamedVariable*> unnamedInRecord;
        visitDepthFirst(*constraint, [&](const RecordInit& record) {
            for (auto* arg : record.getArguments()) {
                if (auto* unnamed = as<UnnamedVariable>(arg)) {
                    unnamedInRecord.insert(unnamed);
                }
            }
        });
 
        // Don't worry about underscores if either side is an aggregate (because of witness exporting)
        if (isA<Aggregator>(*constraint->getLHS()) || isA<Aggregator>(*constraint->getRHS())) {
            return;
        }
        // Check if constraint contains unnamed variables.
        for (auto* unnamed : getUnnamedVariables(*constraint)) {
            if (!contains(unnamedInRecord, unnamed)) {
                report.addError("Underscore in binary relation", unnamed->getSrcLoc());
            }
        }
    }
}
 
/**
 * agg1, agg2 are clauses which contain no head, and consist of a single literal
 * that contains an aggregate.
 * agg1 is dependent on agg2 if agg1 contains a variable which is grounded by agg2, and not by agg1.
 */

checkNamespaces()

void souffle::ast::transform::SemanticCheckerImpl::checkNamespaces ( )

private

Definition at line 995 of file SemanticChecker.cpp.

                                     {
            report.addError("Name clash on type " + name, type->getSrcLoc());
        } else {
            names[name] = type->getSrcLoc();
        }
    }
 
    for (const auto& rel : program.getRelations()) {
        const std::string name = toString(rel->getQualifiedName());
        if (names.count(name) != 0u) {
            report.addError("Name clash on relation " + name, rel->getSrcLoc());
        } else {
            names[name] = rel->getSrcLoc();
        }
    }
}
 
}  // namespace souffle::ast::transform

References souffle::ErrorReport::addError().

Here is the call graph for this function:

checkRelation()

void souffle::ast::transform::SemanticCheckerImpl::checkRelation ( const Relation &  relation )

private

Definition at line 595 of file SemanticChecker.cpp.

               {
            report.addError(
                    "Equivalence relation " + toString(relation.getQualifiedName()) + " is not binary",
                    relation.getSrcLoc());
        }
    }
 
    // start with declaration
    checkRelationDeclaration(relation);
 
    // check whether this relation is empty
    if (getClauses(program, relation).empty() && !ioTypes.isInput(&relation) &&
            !relation.hasQualifier(RelationQualifier::SUPPRESSED)) {
        report.addWarning("No rules/facts defined for relation " + toString(relation.getQualifiedName()),
                relation.getSrcLoc());
    }
}
 
void SemanticCheckerImpl::checkIO() {
    auto checkIO = [&](const Directive* directive) {
        auto* r = getRelation(program, directive->getQualifiedName());
        if (r == nullptr) {
            report.addError(

checkRelationDeclaration()

void souffle::ast::transform::SemanticCheckerImpl::checkRelationDeclaration ( const Relation &  relation )

private

Definition at line 571 of file SemanticChecker.cpp.

                                         { return type->getQualifiedName() == typeName; });
 
        /* check whether type exists */
        if (!typeEnv.isPrimitiveType(typeName) && nullptr == existingType) {
            report.addError(tfm::format("Undefined type in attribute %s", *attr), attr->getSrcLoc());
        }
 
        /* check whether name occurs more than once */
        for (size_t j = 0; j < i; j++) {
            if (attr->getName() == attributes[j]->getName()) {
                report.addError(tfm::format("Doubly defined attribute name %s", *attr), attr->getSrcLoc());
            }
        }
    }
}
 
void SemanticCheckerImpl::checkRelation(const Relation& relation) {
    if (relation.getRepresentation() == RelationRepresentation::EQREL) {
        if (relation.getArity() == 2) {
            const auto& attributes = relation.getAttributes();
            assert(attributes.size() == 2 && "mismatching attribute size and arity");

checkWitnessProblem()

void souffle::ast::transform::SemanticCheckerImpl::checkWitnessProblem ( )

private

Definition at line 692 of file SemanticChecker.cpp.

                                        : usesInvalidWitness(tu, clause, agg)) {
                report.addError(
                        "Witness problem: argument grounded by an aggregator's inner scope is used "
                        "ungrounded in "
                        "outer scope in a count/sum/mean aggregate",
                        invalidArgument);
            }
        });
    });
}
 
/**
 * Find a cycle consisting entirely of inlined relations.
 * If no cycle exists, then an empty vector is returned.
 */
std::vector<QualifiedName> findInlineCycle(const PrecedenceGraphAnalysis& precedenceGraph,

References souffle::ErrorReport::addError().

Here is the call graph for this function:

isDependent()

bool souffle::ast::transform::SemanticCheckerImpl::isDependent ( const Clause &  agg1, const Clause &  agg2  )

private

agg1, agg2 are clauses which contain no head, and consist of a single literal that contains an aggregate.

agg1 is dependent on agg2 if agg1 contains a variable which is grounded by agg2, and not by agg1.

Definition at line 350 of file SemanticChecker.cpp.

                                                          {
            if (var == searchVar) {
                matchingVarPtr = &var;
                return;
            }
        });
        // If the variable occurs in both clauses (a match was found)
        if (matchingVarPtr != nullptr) {
            if (!groundedInAgg1[&searchVar] && groundedInAgg2[matchingVarPtr]) {
                dependent = true;
            }
        }
    });
    return dependent;
}
 
void SemanticCheckerImpl::checkAggregator(const Aggregator& aggregator) {
    auto& report = tu.getErrorReport();
    const Program& program = tu.getProgram();
    Clause dummyClauseAggregator;
 

Field Documentation

ioTypes

const IOTypeAnalysis& souffle::ast::transform::SemanticCheckerImpl::ioTypes = *tu.getAnalysis<IOTypeAnalysis>()

private

Definition at line 113 of file SemanticChecker.cpp.

precedenceGraph

const PrecedenceGraphAnalysis& souffle::ast::transform::SemanticCheckerImpl::precedenceGraph = *tu.getAnalysis<PrecedenceGraphAnalysis>()

private

Definition at line 114 of file SemanticChecker.cpp.

program

const Program& souffle::ast::transform::SemanticCheckerImpl::program = tu.getProgram()

private

Definition at line 120 of file SemanticChecker.cpp.

Referenced by SemanticCheckerImpl().

recursiveClauses

const RecursiveClausesAnalysis& souffle::ast::transform::SemanticCheckerImpl::recursiveClauses = *tu.getAnalysis<RecursiveClausesAnalysis>()

private

Definition at line 115 of file SemanticChecker.cpp.

report

ErrorReport& souffle::ast::transform::SemanticCheckerImpl::report = tu.getErrorReport()

private

Definition at line 121 of file SemanticChecker.cpp.

Referenced by checkBranchInits().

sccGraph

const SCCGraphAnalysis& souffle::ast::transform::SemanticCheckerImpl::sccGraph = *tu.getAnalysis<SCCGraphAnalysis>()

private

Definition at line 116 of file SemanticChecker.cpp.

sumTypesBranches

const SumTypeBranchesAnalysis& souffle::ast::transform::SemanticCheckerImpl::sumTypesBranches = *tu.getAnalysis<SumTypeBranchesAnalysis>()

private

Definition at line 117 of file SemanticChecker.cpp.

tu

TranslationUnit& souffle::ast::transform::SemanticCheckerImpl::tu

Definition at line 109 of file SemanticChecker.cpp.

typeEnv

const TypeEnvironment& souffle::ast::transform::SemanticCheckerImpl::typeEnv = tu.getAnalysis<TypeEnvironmentAnalysis>()->getTypeEnvironment()

private

Definition at line 119 of file SemanticChecker.cpp.

---

The documentation for this struct was generated from the following file:

• ast/transform/SemanticChecker.cpp