souffle::ast::analysis Namespace Reference

Namespaces
	detail

Data Structures
class	AlgebraicDataType
	Aggregates types using sums and products. More...
struct	all_type_factory
	A factory for computing sets of types covering all potential types. More...
class	Analysis
	Abstract class for a AST Analysis. More...
class	Assignment
	An assignment maps a list of variables to values of their respective property space. More...
class	AuxiliaryArityAnalysis
	Determine the auxiliary arity for relations. More...
class	ClauseNormalisationAnalysis
class	ComponentLookupAnalysis
class	ConstantType
	Representing the type assigned to a constant. More...
class	Constraint
	A generic base class for constraints on variables. More...
class	ConstraintAnalysis
	A base class for ConstraintAnalysis collecting constraints for an analysis by visiting every node of a given AST. More...
struct	ConstraintAnalysisVar
	A variable type to be utilized by AST constraint analysis. More...
class	FunctorAnalysis
class	IOTypeAnalysis
class	NormalisedClause
class	PolymorphicObjectsAnalysis
class	PrecedenceGraphAnalysis
	Analysis pass computing the precedence graph of the relations of the datalog progam. More...
class	PrimitiveType
	PrimitiveType = Number/Unsigned/Float/Symbol The class representing pre-built, concrete types. More...
class	Problem
	A problem is a list of constraints for which a solution is desired. More...
class	ProfileUseAnalysis
	Analysis that loads profile data and has a profile query interface. More...
struct	property_space
	A MPL type for defining a property space. More...
struct	RecordType
	A record type combining a list of fields into a new, aggregated type. More...
class	RecursiveClausesAnalysis
	Analysis pass identifying clauses which are recursive. More...
class	RedundantRelationsAnalysis
	Analysis pass identifying relations which do not contribute to the computation of the output relations. More...
class	RelationDetailCacheAnalysis
	Analysis pass mapping identifiers with relations and clauses. More...
class	RelationScheduleAnalysis
	Analysis pass computing a schedule for computing relations. More...
class	RelationScheduleAnalysisStep
	A single step in a relation schedule, consisting of the relations computed in the step and the relations that are no longer required at that step. More...
class	SCCGraphAnalysis
	Analysis pass computing the strongly connected component (SCC) graph for the datalog program. More...
struct	set_property_space
	A property space for set-based properties based on sub-set lattices. More...
struct	sub_type
	An implementation of a meet operation between sets of types computing the set of pair-wise greatest common subtypes. More...
class	SubsetType
	A type being a subset of another type. More...
class	SumTypeBranchesAnalysis
class	TopologicallySortedSCCGraphAnalysis
	Analysis pass computing a topologically sorted strongly connected component (SCC) graph. More...
class	Type
	An abstract base class for types to be covered within a type environment. More...
struct	type_lattice
	The type lattice forming the property space for the Type analysis. More...
class	TypeAnalysis
class	TypeBinding
	Class that encapsulates std::map of types binding that comes from .init c = Comp<MyType> Type binding in this example would be T->MyType if the component code is .comp Comp<T> ... More...
class	TypeConstraintsAnalysis
	Constraint analysis framework for types. More...
class	TypeEnvironment
	A type environment is a set of types. More...
class	TypeEnvironmentAnalysis
struct	TypeSet
	A collection to represent sets of types. More...
struct	TypeVisitor
	A visitor for Types. More...
class	UnionType
	A union type combining a list of types into a new, aggregated type. More...
struct	Variable
	A variable to be utilized within constraints to be handled by the constraint solver. More...
class	VisitOnceTypeVisitor
	A visitor for types visiting each type only once (effectively breaking recursive cycles). More...

Typedefs
using	TypeConstraint = std::shared_ptr< Constraint< TypeVar > >
	The definition of the type of constraint to be utilized in the type analysis. More...
using	TypeVar = ConstraintAnalysisVar< type_lattice >
	The definition of the type of variable to be utilized in the type analysis. More...

Functions
bool	areEquivalentTypes (const Type &a, const Type &b)
	Determine if two types are equivalent. More...
std::string	findUniqueRelationName (const Program &program, std::string base)
	Find a new relation name. More...
std::string	findUniqueVariableName (const Clause &clause, std::string base)
	Find a variable name using base to form a string like base1 Use this when you need to limit the scope of a variable to the inside of an aggregate. More...
static const Type &	getBaseType (const Type *type)
TypeSet	getGreatestCommonSubtypes (const Type &a, const Type &b)
	Computes the greatest common sub types of the two given types. More...
template<typename... Types>
TypeSet	getGreatestCommonSubtypes (const Types &... types)
	Computes the greatest common sub types of the given types. More...
TypeSet	getGreatestCommonSubtypes (const TypeSet &a, const TypeSet &b)
	The set of pair-wise greatest common sub types of the types in the two given sets. More...
TypeSet	getGreatestCommonSubtypes (const TypeSet &set)
	Computes the greatest common sub types of all the types in the given set. More...
std::map< const Argument *, bool >	getGroundedTerms (const TranslationUnit &tu, const Clause &clause)
	Analyse the given clause and computes for each contained argument whether it is a grounded value or not. More...
std::set< std::string >	getInjectedVariables (const TranslationUnit &tu, const Clause &clause, const Aggregator &aggregate)
	Given an aggregate and a clause, we find all the variables that have been injected into the aggregate. More...
std::set< std::string >	getLocalVariables (const TranslationUnit &tu, const Clause &clause, const Aggregator &aggregate)
	Computes the set of local variables in an aggregate expression. More...
TypeAttribute	getTypeAttribute (const Type &type)
std::optional< TypeAttribute >	getTypeAttribute (const TypeSet &type)
std::string	getTypeQualifier (const Type &type)
	Returns full type qualifier for a given type. More...
std::set< std::string >	getVariablesOutsideAggregate (const Clause &clause, const Aggregator &aggregate)
	Computes the set of variables occurring outside the aggregate. More...
std::set< std::string >	getWitnessVariables (const TranslationUnit &tu, const Clause &clause, const Aggregator &aggregate)
	Computes the set of witness variables that are used in the aggregate A variable is a witness if it occurs in the aggregate body (but not in an inner aggregate) and also occurs ungrounded in the outer scope. More...
static TypeConstraint	hasSuperTypeInSet (const TypeVar &var, TypeSet values)
	A constraint factory ensuring that all the types associated to the variable are subtypes of some type in the provided set (values) More...
bool	haveCommonSupertype (const Type &a, const Type &b)
	Determine if there exist a type t such that a <: t and b <: t. More...
bool	isADTEnum (const AlgebraicDataType &type)
	Determine if ADT is enumerations (are all constructors empty) More...
bool	isNumericType (const TypeSet &type)
bool	isOfKind (const Type &type, TypeAttribute kind)
	Check if the type is of a kind corresponding to the TypeAttribute. More...
bool	isOfKind (const TypeSet &typeSet, TypeAttribute kind)
bool	isOfRootType (const Type &type, const Type &root)
	Determines whether the given type is a sub-type of the given root type. More...
bool	isOrderableType (const TypeSet &type)
bool	isSubtypeOf (const Type &a, const Type &b)
	Determines whether type a is a subtype of type b. More...
static TypeConstraint	isSubtypeOf (const TypeVar &a, const TypeVar &b)
	A constraint factory ensuring that all the types associated to the variable a are subtypes of the variable b. More...
static TypeConstraint	isSubtypeOf (const TypeVar &variable, const Type &type)
	A constraint factory ensuring that all the types associated to the variable a are subtypes of type b. More...
static TypeConstraint	isSubtypeOfComponent (const TypeVar &elementVariable, const TypeVar &recordVariable, size_t index)
	Constraint on record type and its elements. More...
static TypeConstraint	satisfiesOverload (const TypeEnvironment &typeEnv, IntrinsicFunctors overloads, TypeVar result, std::vector< TypeVar > args, bool subtypeResult)
	Given a set of overloads, wait the list of candidates to reduce to one and then apply its constraints. More...
template<typename Var , typename Val = typename Var::property_space::value_type>
std::shared_ptr< Constraint< Var > >	sub (const Val &a, const Var &b, const std::string &symbol="⊑")
	A generic factory for constraints of the form. More...
template<typename Var >
std::shared_ptr< Constraint< Var > >	sub (const Var &a, const Var &b, const std::string &symbol="⊑")
	A generic factory for constraints of the form. More...
static TypeConstraint	subtypesOfTheSameBaseType (const TypeVar &left, const TypeVar &right)
	Ensure that types of left and right have the same base types. More...

Typedef Documentation

TypeConstraint

using souffle::ast::analysis::TypeConstraint = typedef std::shared_ptr<Constraint<TypeVar> >

The definition of the type of constraint to be utilized in the type analysis.

Definition at line 75 of file TypeConstraints.h.

TypeVar

using souffle::ast::analysis::TypeVar = typedef ConstraintAnalysisVar<type_lattice>

The definition of the type of variable to be utilized in the type analysis.

Definition at line 72 of file TypeConstraints.h.

Function Documentation

areEquivalentTypes()

bool souffle::ast::analysis::areEquivalentTypes	(	const Type &	a,
		const Type &	b
	)

Determine if two types are equivalent.

That is, check if a <: b and b <: a

Definition at line 373 of file TypeSystem.cpp.

findUniqueRelationName()

std::string souffle::ast::analysis::findUniqueRelationName	(	const Program &	program,
		std::string	base
	)

Find a new relation name.

I use this when I create new relations either for aggregate bodies or singleton aggregates.

Definition at line 190 of file Aggregate.cpp.

findUniqueVariableName()

std::string souffle::ast::analysis::findUniqueVariableName	(	const Clause &	clause,
		std::string	base
	)

Find a variable name using base to form a string like base1 Use this when you need to limit the scope of a variable to the inside of an aggregate.

Definition at line 179 of file Aggregate.cpp.

                                                                         {
    int counter = 0;
    auto candidate = base;
    while (getRelation(program, candidate) != nullptr) {
        candidate = base + toString(counter++);

Referenced by souffle::ast::transform::SimplifyAggregateTargetExpressionTransformer::transform().

getBaseType()

static const Type& souffle::ast::analysis::getBaseType ( const Type *  type )

static

Definition at line 118 of file TypeConstraints.cpp.

                                                                                           {

getGreatestCommonSubtypes() [1/4]

TypeSet souffle::ast::analysis::getGreatestCommonSubtypes	(	const Type &	a,
		const Type &	b
	)

Computes the greatest common sub types of the two given types.

Definition at line 254 of file TypeSystem.cpp.

                           {
        return TypeSet(b);
    }
 
    TypeSet res;
    if (isA<UnionType>(a) && isA<UnionType>(b)) {
        // collect common sub-types of union types
        struct collector : public TypeVisitor<void> {
            const Type& b;
            TypeSet& res;
            collector(const Type& b, TypeSet& res) : b(b), res(res) {}
 
            void visit(const Type& type) const override {
                if (isSubtypeOf(type, b)) {
                    res.insert(type);
                } else {
                    TypeVisitor<void>::visit(type);
                }
            }
            void visitUnionType(const UnionType& type) const override {
                for (const auto& cur : type.getElementTypes()) {
                    visit(*cur);
                }
            }
        };
 
        // collect all common sub-types
        collector(b, res).visit(a);
    }
 
    // otherwise there is no common super type
    return res;
}
 
TypeSet getGreatestCommonSubtypes(const TypeSet& set) {
    // Edge cases.
    if (set.empty() || set.isAll()) {
        return TypeSet();
    }

Referenced by getGreatestCommonSubtypes().

getGreatestCommonSubtypes() [2/4]

template<typename... Types>

TypeSet souffle::ast::analysis::getGreatestCommonSubtypes

(

const Types &...

types

)

Computes the greatest common sub types of the given types.

Definition at line 542 of file TypeSystem.h.

getGreatestCommonSubtypes() [3/4]

TypeSet souffle::ast::analysis::getGreatestCommonSubtypes	(	const TypeSet &	a,
		const TypeSet &	b
	)

The set of pair-wise greatest common sub types of the types in the two given sets.

Definition at line 311 of file TypeSystem.cpp.

                   {
        return b;
    }
    if (b.isAll()) {
        return a;
    }
 
    // compute pairwise greatest common sub types
    TypeSet res;
    for (const Type& x : a) {
        for (const Type& y : b) {
            res.insert(getGreatestCommonSubtypes(x, y));
        }
    }
    return res;
}
 
bool haveCommonSupertype(const Type& a, const Type& b) {
    assert(&a.getTypeEnvironment() == &b.getTypeEnvironment() &&
            "Types must be in the same type environment");
 
    if (a == b) {

getGreatestCommonSubtypes() [4/4]

TypeSet souffle::ast::analysis::getGreatestCommonSubtypes

(

const TypeSet &

set

)

Computes the greatest common sub types of all the types in the given set.

Definition at line 295 of file TypeSystem.cpp.

                    : set) {
        greatestCommonSubtypes = getGreatestCommonSubtypes(TypeSet(type), greatestCommonSubtypes);
    }
 
    return greatestCommonSubtypes;
}
 
TypeSet getGreatestCommonSubtypes(const TypeSet& a, const TypeSet& b) {
    // special cases
    if (a.empty()) {
        return a;
    }

References getGreatestCommonSubtypes().

Here is the call graph for this function:

getGroundedTerms()

std::map< const Argument *, bool > souffle::ast::analysis::getGroundedTerms	(	const TranslationUnit &	tu,
		const Clause &	clause
	)

Analyse the given clause and computes for each contained argument whether it is a grounded value or not.

Parameters

tu	the translation unit containing the clause
clause	the clause to be analyzed

Returns

a map mapping each contained argument to a boolean indicating whether the argument represents a grounded value or not

Definition at line 278 of file Ground.cpp.

getInjectedVariables()

std::set< std::string > souffle::ast::analysis::getInjectedVariables	(	const TranslationUnit &	tu,
		const Clause &	clause,
		const Aggregator &	aggregate
	)

Given an aggregate and a clause, we find all the variables that have been injected into the aggregate.

This means that the variable occurs grounded in an outer scope. BUT does not occur in the target expression.

This means that the variable occurs grounded in an outer scope.

Imagine we have this:

A(letter, x) :- a(letter, _), x = min y : { a(l, y), y < max y : { a(letter, y) } }, z = max y : {B(y) }.

We need to figure out the base literal in which this aggregate occurs, so that we don't delete them Other aggregates occurring in the rule are irrelevant, so we'll replace the aggregate with a dummy aggregate variable. Then after that,

1. A(letter, x) :- a(letter, _), x = min y : { a(l, y), y < max y : { a(letter, y) } }, z = aggr_var_0.

We should also ground all the aggr_vars so that this grounding transfers to whatever variable they might be assigned to.

A(letter, x) :- a(letter, _), x = min y : { a(l, y), y < max y : { a(letter, y) } }, z = aggr_var_0, grounding_atom(aggr_var_0).

Remember to negate the head atom and add it to the body. The clause we deal with will have a dummy head (*())

*() :- !A(letter, x), a(letter, _), x = min y : { a(l, y), y < max y : { a(letter, y) } }, z = aggr_var_0, grounding_atom(aggr_var_0).

Replace the original aggregate with the same shit because we can't be counting local variables n shit

*() :- !A(letter, x), a(letter, _), x = min y : { a(l, y), y < aggr_var_1 } }, z = aggr_var_0, grounding_atom(aggr_var_0).

Now, as long as we recorded all of the variables that occurred inside the aggregate, the intersection of these two sets (variables in an outer scope) and (variables occurring in t

A variable is considered injected into an aggregate if it occurs both within the aggregate AS WELL AS grounded in the outer scope. An outer scope could be an outer aggregate, or also just the base/rule scope. (i.e. not inside of another aggregate that is not an ancestor of this one).

So then in order to calculate the set of variables that have been injected into an aggregate, we perform the following steps:

1. Find the set of variables occurring within the aggregate "aggregate"
2. Find the set of variables that occur grounded in the outside scope 2a. Replace all non-ancestral aggregates with variables so that we can ignore their variable contents (it is not relevant). 2b. Replace the target aggregate with a variable as well 2c. Ground all occurrences of the non-ancestral aggregate variable replacements (i.e. grounding_atom(+aggr_var_0)) 2d. Visit all variables occurring in this tweaked clause that we made from steps 2a-2c, and check if they are grounded, and also occur in the set of target aggregate variables. Then it is an injected variable.

Definition at line 205 of file Aggregate.cpp.

                       : { a(l, y),
     *       y < max y : { a(letter, y) } },
     *       z = max y : {B(y) }.
     *
     *   We need to figure out the base literal in which this aggregate occurs,
     *   so that we don't delete them
     *   Other aggregates occurring in the rule are irrelevant, so we'll replace
     *   the aggregate with a dummy aggregate variable. Then after that,
     *
     *   2. A(letter, x) :-
     *       a(letter, _),
     *       x = min y : { a(l, y),
     *       y < max y : { a(letter, y) } },
     *       z = aggr_var_0.
     *
     *   We should also ground all the aggr_vars so that this grounding
     *   transfers to whatever variable they might be assigned to.
     *
     *   A(letter, x) :-
     *       a(letter, _),
     *       x = min y : { a(l, y),
     *       y < max y : { a(letter, y) } },
     *       z = aggr_var_0,
     *       grounding_atom(aggr_var_0).
     *
     *   Remember to negate the head atom and add it to the body. The clause we deal with will have a
     *   dummy head (*())
     *
     *    *() :- !A(letter, x), a(letter, _), x = min y : { a(l, y), y < max y : { a(letter, y) } },
     *        z = aggr_var_0, grounding_atom(aggr_var_0).
     *
     *   Replace the original aggregate with the same shit because we can't be counting local variables n shit
     *
     *    *() :- !A(letter, x), a(letter, _), x = min y : { a(l, y), y < aggr_var_1 } }, z = aggr_var_0,
     *        grounding_atom(aggr_var_0).
     *
     *   Now, as long as we recorded all of the variables that occurred inside the aggregate, the intersection
     *   of these two sets (variables in an outer scope) and (variables occurring in t
     **/
 
    /**
     * A variable is considered *injected* into an aggregate if it occurs both within the aggregate AS WELL
     * AS *grounded* in the outer scope. An outer scope could be an outer aggregate, or also just the
     *base/rule scope. (i.e. not inside of another aggregate that is not an ancestor of this one).
     *
     *   So then in order to calculate the set of variables that have been injected into an aggregate, we
     * perform the following steps:
     *
     *   1. Find the set of variables occurring within the aggregate "aggregate"
     *   2. Find the set of variables that occur grounded in the outside scope
     *       2a. Replace all non-ancestral aggregates with variables so that we can ignore their variable
     * contents (it is not relevant). 2b. Replace the target aggregate with a variable as well 2c. Ground all
     * occurrences of the non-ancestral aggregate variable replacements (i.e. grounding_atom(+aggr_var_0)) 2d.
     * Visit all variables occurring in this tweaked clause that we made from steps 2a-2c, and check if they
     * are grounded, and also occur in the set of target aggregate variables. Then it is an injected variable.
     **/
    // Step 1
    std::set<std::string> variablesInTargetAggregate;
    visitDepthFirst(aggregate,
            [&](const Variable& variable) { variablesInTargetAggregate.insert(variable.getName()); });
 
    std::set<Own<Aggregator>> ancestorAggregates;
 
    visitDepthFirst(clause, [&](const Aggregator& ancestor) {
        visitDepthFirst(ancestor, [&](const Aggregator& agg) {
            if (agg == aggregate) {
                ancestorAggregates.insert(souffle::clone(&ancestor));
            }
        });
    });
 
    // 1. Replace non-ancestral aggregates with variables
    struct ReplaceAggregatesWithVariables : public NodeMapper {
        // Variables introduced to replace aggregators
        mutable std::set<std::string> aggregatorVariables;
        // ancestors are never replaced so don't need to clone, but actually
        // it will have a child that will become invalid at one point. This is a concern. Need to clone these
        // bastards too.
        std::set<Own<Aggregator>> ancestors;
        // make sure you clone the agg first.
        Own<Aggregator> targetAggregate;
 
        const std::set<std::string>& getAggregatorVariables() {
            return aggregatorVariables;
        }
 
        ReplaceAggregatesWithVariables(std::set<Own<Aggregator>> ancestors, Own<Aggregator> targetAggregate)
                : ancestors(std::move(ancestors)), targetAggregate(std::move(targetAggregate)) {}
 
        std::unique_ptr<Node> operator()(std::unique_ptr<Node> node) const override {
            static int numReplaced = 0;
            if (auto* aggregate = dynamic_cast<Aggregator*>(node.get())) {
                // If we come across an aggregate that is NOT an ancestor of
                // the target aggregate, or that IS itself the target aggregate,
                // we should replace it with a dummy variable.
                bool isAncestor = false;
                for (auto& ancestor : ancestors) {
                    if (*ancestor == *aggregate) {
                        isAncestor = true;
                        break;
                    }
                }
                if (!isAncestor || *aggregate == *targetAggregate) {
                    // Replace the aggregator with a variable
                    std::stringstream newVariableName;
                    newVariableName << "+aggr_var_" << numReplaced++;
                    // Keep track of which variables are bound to aggregators
                    // (only applicable to non-ancestral aggregates)
                    if (!isAncestor) {
                        // we don't want to ground the target aggregate
                        // (why?) because these variables could be injected
                        // and that is fine.
                        aggregatorVariables.insert(newVariableName.str());
                        // but we are not supposed to be judging the aggregate as grounded and injected into
                        // the aggregate, that wouldn't make sense
                    }
                    return mk<Variable>(newVariableName.str());
                }
            }
            node->apply(*this);
            return node;
        }
    };
    // 2. make a clone of the clause and then apply that mapper onto it
    auto clauseCopy = souffle::clone(&clause);
    auto tweakedClause = mk<Clause>();
    // put a fake head here
    tweakedClause->setHead(mk<Atom>("*"));
    // copy in all the old body literals
    for (Literal* lit : clause.getBodyLiterals()) {
        tweakedClause->addToBody(souffle::clone(lit));
    }
    // copy in the head as a negated atom
    tweakedClause->addToBody(mk<Negation>(souffle::clone(clause.getHead())));
    // copy in body literals and also add the old head as a negated atom
    ReplaceAggregatesWithVariables update(std::move(ancestorAggregates), souffle::clone(&aggregate));
    tweakedClause->apply(update);
    // the update will now tell us which variables we need to ground!
    auto groundingAtom = mk<Atom>("+grounding_atom");
    for (std::string variableName : update.getAggregatorVariables()) {
        groundingAtom->addArgument(mk<Variable>(variableName));
    }
    // add the newly created grounding atom to the body
    tweakedClause->addToBody(std::move(groundingAtom));
 
    std::set<std::string> injectedVariables;
    // Search through the tweakedClause to find groundings!
    for (const auto& argPair : analysis::getGroundedTerms(tu, *tweakedClause)) {
        if (const auto* variable = dynamic_cast<const Variable*>(argPair.first)) {
            bool varIsGrounded = argPair.second;
            if (varIsGrounded && variablesInTargetAggregate.find(variable->getName()) !=
                                         variablesInTargetAggregate.end()) {
                // then we have found an injected variable, lovely!!
                injectedVariables.insert(variable->getName());
            }
        }
    }
    // Remove any variables that occur in the target expression of the aggregate
    if (aggregate.getTargetExpression() != nullptr) {
        visitDepthFirst(*aggregate.getTargetExpression(),
                [&](const Variable& v) { injectedVariables.erase(v.getName()); });
    }
 
    return injectedVariables;
}
 
}  // namespace souffle::ast::analysis

getLocalVariables()

std::set< std::string > souffle::ast::analysis::getLocalVariables	(	const TranslationUnit &	tu,
		const Clause &	clause,
		const Aggregator &	aggregate
	)

Computes the set of local variables in an aggregate expression.

This is just the set of all variables occurring in the aggregate MINUS the injected variables MINUS the witness variables. :)

Definition at line 55 of file Aggregate.cpp.

                               : allVariablesInAggregate) {
        if (injectedVariables.find(name) == injectedVariables.end() &&
                witnessVariables.find(name) == witnessVariables.end()) {
            localVariables.insert(name);
        }
    }
    return localVariables;
}
/**
 * Computes the set of witness variables that are used in the aggregate
 * A variable is a witness if it occurs in the aggregate body (but not in an inner aggregate)
 * and also occurs ungrounded in the outer scope.
 **/
std::set<std::string> getWitnessVariables(

getTypeAttribute() [1/2]

TypeAttribute souffle::ast::analysis::getTypeAttribute

(

const Type &

type

)

Definition at line 353 of file TypeSystem.cpp.

                                                                 {
    for (auto typeAttribute : {TypeAttribute::Signed, TypeAttribute::Unsigned, TypeAttribute::Float,
                 TypeAttribute::Record, TypeAttribute::Symbol}) {
        if (isOfKind(type, typeAttribute)) {
            return typeAttribute;

getTypeAttribute() [2/2]

std::optional< TypeAttribute > souffle::ast::analysis::getTypeAttribute

(

const TypeSet &

type

)

Definition at line 363 of file TypeSystem.cpp.

           {};
}
 
bool areEquivalentTypes(const Type& a, const Type& b) {
    return isSubtypeOf(a, b) && isSubtypeOf(b, a);
}
 
bool isADTEnum(const AlgebraicDataType& type) {

getTypeQualifier()

std::string souffle::ast::analysis::getTypeQualifier

(

const Type &

type

)

Returns full type qualifier for a given type.

Definition at line 204 of file TypeSystem.cpp.

                                                       {
            return "f";
        } else if (isOfKind(type, TypeAttribute::Symbol)) {
            return "s";
        } else if (isOfKind(type, TypeAttribute::Record)) {
            return "r";
        } else if (isOfKind(type, TypeAttribute::ADT)) {
            return "+";
        } else {
            fatal("Unsupported kind");
        }
    }();
 
    return tfm::format("%s:%s", kind, type.getName());
}
 
bool isSubtypeOf(const Type& a, const Type& b) {
    assert(&a.getTypeEnvironment() == &b.getTypeEnvironment() &&
            "Types must be in the same type environment");
 
    if (isOfRootType(a, b)) {

Referenced by souffle::ast::transform::IOAttributesTransformer::getRecordsTypes().

getVariablesOutsideAggregate()

std::set< std::string > souffle::ast::analysis::getVariablesOutsideAggregate	(	const Clause &	clause,
		const Aggregator &	aggregate
	)

Computes the set of variables occurring outside the aggregate.

Find the set of variable names occurring outside of the given aggregate.

This is equivalent to taking the set minus of the set of all variable names occurring in the clause minus the set of all variable names occurring in the aggregate.

Definition at line 164 of file Aggregate.cpp.

                                {
            variablesOutsideAggregate.insert(v);
        }
    }
    return variablesOutsideAggregate;
}
 
std::string findUniqueVariableName(const Clause& clause, std::string base) {
    std::set<std::string> variablesInClause;
    visitDepthFirst(clause, [&](const Variable& v) { variablesInClause.insert(v.getName()); });
    int varNum = 0;
    std::string candidate = base;

Referenced by souffle::ast::transform::SimplifyAggregateTargetExpressionTransformer::transform().

getWitnessVariables()

std::set< std::string > souffle::ast::analysis::getWitnessVariables	(	const TranslationUnit &	tu,
		const Clause &	clause,
		const Aggregator &	aggregate
	)

Computes the set of witness variables that are used in the aggregate A variable is a witness if it occurs in the aggregate body (but not in an inner aggregate) and also occurs ungrounded in the outer scope.

Computes the set of witness variables that are used in the aggregate.

Definition at line 75 of file Aggregate.cpp.

                                                          {
            return aggregatorVariables;
        }
 
        std::unique_ptr<Node> operator()(std::unique_ptr<Node> node) const override {
            static int numReplaced = 0;
            if (dynamic_cast<Aggregator*>(node.get()) != nullptr) {
                // Replace the aggregator with a variable
                std::stringstream newVariableName;
                newVariableName << "+aggr_var_" << numReplaced++;
 
                // Keep track of which variables are bound to aggregators
                aggregatorVariables.insert(newVariableName.str());
 
                return std::make_unique<Variable>(newVariableName.str());
            }
            node->apply(*this);
            return node;
        }
    };
 
    auto aggregatorlessClause = std::make_unique<Clause>();
    aggregatorlessClause->setHead(std::make_unique<Atom>("*"));
    for (Literal* lit : clause.getBodyLiterals()) {
        aggregatorlessClause->addToBody(souffle::clone(lit));
    }
 
    auto negatedHead = std::make_unique<Negation>(souffle::clone(clause.getHead()));
    aggregatorlessClause->addToBody(std::move(negatedHead));
 
    // Replace all aggregates with variables
    M update;
    aggregatorlessClause->apply(update);
    auto groundingAtom = std::make_unique<Atom>("+grounding_atom");
    for (std::string variableName : update.getAggregatorVariables()) {
        groundingAtom->addArgument(std::make_unique<Variable>(variableName));
    }
    aggregatorlessClause->addToBody(std::move(groundingAtom));
    // 2. Create an aggregate clause so that we can check
    // that it IS this aggregate giving a grounding to the candidate variable.
    auto aggregateSubclause = std::make_unique<Clause>();
    aggregateSubclause->setHead(mk<Atom>("*"));
    for (const auto& lit : aggregate.getBodyLiterals()) {
        aggregateSubclause->addToBody(souffle::clone(lit));
    }
 
    std::set<std::string> witnessVariables;
    auto isGroundedInAggregateSubclause = analysis::getGroundedTerms(tu, *aggregateSubclause);
    // 3. Calculate all the witness variables
    // A witness will occur ungrounded in the aggregatorlessClause
    for (const auto& argPair : analysis::getGroundedTerms(tu, *aggregatorlessClause)) {
        if (const auto* variable = dynamic_cast<const Variable*>(argPair.first)) {
            bool variableIsGrounded = argPair.second;
            if (!variableIsGrounded) {
                // then we expect it to be grounded in the aggregate subclause
                // if it's a witness!!
                for (const auto& aggArgPair : isGroundedInAggregateSubclause) {
                    if (const auto* var = dynamic_cast<const Variable*>(aggArgPair.first)) {
                        bool aggVariableIsGrounded = aggArgPair.second;
                        if (var->getName() == variable->getName() && aggVariableIsGrounded) {
                            witnessVariables.insert(variable->getName());
                        }
                    }
                }
            }
        }
    }
    // 4. A witness variable may actually "originate" from an outer scope and
    // just have been injected into this inner aggregate. Just check the set of injected variables
    // and quickly minus them out.
    std::set<std::string> injectedVariables = analysis::getInjectedVariables(tu, clause, aggregate);
    for (const std::string& injected : injectedVariables) {
        witnessVariables.erase(injected);
    }
 
    return witnessVariables;
}
/**
 *  Computes the set of variables occurring outside the aggregate
 **/
std::set<std::string> getVariablesOutsideAggregate(const Clause& clause, const Aggregator& aggregate) {
    std::map<std::string, int> variableOccurrences;
    visitDepthFirst(clause, [&](const Variable& var) { variableOccurrences[var.getName()]++; });

Referenced by souffle::ast::transform::SimplifyAggregateTargetExpressionTransformer::transform().

hasSuperTypeInSet()

static TypeConstraint souffle::ast::analysis::hasSuperTypeInSet ( const TypeVar &  var, TypeSet  values  )

static

A constraint factory ensuring that all the types associated to the variable are subtypes of some type in the provided set (values)

Values can't be all.

Definition at line 77 of file TypeConstraints.cpp.

                                       : var(std::move(var)), values(std::move(values)) {}
 
        bool update(Assignment<TypeVar>& assigment) const override {
            // get current value of variable a
            TypeSet& assigments = assigment[var];
 
            // remove all types that are not sub-types of b
            if (assigments.isAll()) {
                assigments = values;
                return true;
            }
 
            TypeSet newAssigments;
            for (const Type& type : assigments) {
                bool existsSuperTypeInValues =
                        any_of(values, [&type](const Type& value) { return isSubtypeOf(type, value); });
                if (existsSuperTypeInValues) {
                    newAssigments.insert(type);
                }
            }
            // check whether there was a change
            if (newAssigments == assigments) {
                return false;
            }
            assigments = newAssigments;
            return true;
        }
 
        void print(std::ostream& out) const override {
            out << "∃ t ∈ " << values << ": " << var << " <: t";
        }
    };
 
    return std::make_shared<C>(var, values);
}
 
static const Type& getBaseType(const Type* type) {
    while (auto subset = dynamic_cast<const SubsetType*>(type)) {
        type = &subset->getBaseType();

haveCommonSupertype()

bool souffle::ast::analysis::haveCommonSupertype	(	const Type &	a,
		const Type &	b
	)

Determine if there exist a type t such that a <: t and b <: t.

Definition at line 337 of file TypeSystem.cpp.

                                                {
        return true;
    }
 
    return any_of(a.getTypeEnvironment().getTypes(),
            [&](const Type& type) { return isSubtypeOf(a, type) && isSubtypeOf(b, type); });
}
 
TypeAttribute getTypeAttribute(const Type& type) {
    for (auto typeAttribute : {TypeAttribute::Signed, TypeAttribute::Unsigned, TypeAttribute::Float,
                 TypeAttribute::Record, TypeAttribute::Symbol}) {
        if (isOfKind(type, typeAttribute)) {
            return typeAttribute;

isADTEnum()

bool souffle::ast::analysis::isADTEnum

(

const AlgebraicDataType &

type

)

Determine if ADT is enumerations (are all constructors empty)

Definition at line 377 of file TypeSystem.cpp.

isNumericType()

bool souffle::ast::analysis::isNumericType ( const TypeSet &  type )

inline

Definition at line 512 of file TypeSystem.h.

                                                         {

isOfKind() [1/2]

bool souffle::ast::analysis::isOfKind	(	const Type &	type,
		TypeAttribute	kind
	)

Check if the type is of a kind corresponding to the TypeAttribute.

Definition at line 189 of file TypeSystem.cpp.

                                                          {
    return !typeSet.empty() && !typeSet.isAll() &&
           all_of(typeSet, [&](const Type& type) { return isOfKind(type, kind); });
}
 

Referenced by isOfKind(), and souffle::ast::transform::TypeCheckerImpl::visitVariable().

isOfKind() [2/2]

bool souffle::ast::analysis::isOfKind	(	const TypeSet &	typeSet,
		TypeAttribute	kind
	)

Definition at line 199 of file TypeSystem.cpp.

                           {
        if (isOfKind(type, TypeAttribute::Signed)) {
            return "i";
        } else if (isOfKind(type, TypeAttribute::Unsigned)) {

References isOfKind(), souffle::Signed, and souffle::Unsigned.

Here is the call graph for this function:

isOfRootType()

bool souffle::ast::analysis::isOfRootType	(	const Type &	type,
		const Type &	root
	)

Determines whether the given type is a sub-type of the given root type.

Definition at line 155 of file TypeSystem.cpp.

                                                                        {
            return type == root;
        }
        bool visitSubsetType(const SubsetType& type) const override {
            return type == root || isOfRootType(type.getBaseType(), root);
        }
 
        bool visitAlgebraicDataType(const AlgebraicDataType& type) const override {
            return type == root;
        }
 
        bool visitUnionType(const UnionType& type) const override {
            return type == root ||
                   all_of(type.getElementTypes(), [&](const Type* cur) { return this->visit(*cur); });
        }
 
        bool visitRecordType(const RecordType& type) const override {
            return type == root;
        }
 
        bool visitType(const Type& /*unused*/) const override {
            return false;
        }
    };
 
    return visitor(root).visit(type);
}
 
bool isOfKind(const Type& type, TypeAttribute kind) {
    if (kind == TypeAttribute::Record) {
        return isA<RecordType>(type);
    } else if (kind == TypeAttribute::ADT) {
        return isA<AlgebraicDataType>(type);

isOrderableType()

bool souffle::ast::analysis::isOrderableType ( const TypeSet &  type )

inline

Definition at line 517 of file TypeSystem.h.

                                                         {

isSubtypeOf() [1/3]

bool souffle::ast::analysis::isSubtypeOf	(	const Type &	a,
		const Type &	b
	)

Determines whether type a is a subtype of type b.

Definition at line 226 of file TypeSystem.cpp.

                           {
        return all_of(static_cast<const UnionType&>(a).getElementTypes(),
                [&b](const Type* type) { return isSubtypeOf(*type, b); });
    }
 
    if (isA<UnionType>(b)) {
        return any_of(static_cast<const UnionType&>(b).getElementTypes(),
                [&a](const Type* type) { return isSubtypeOf(a, *type); });
    }
 
    return false;
}
 
void TypeEnvironment::print(std::ostream& out) const {
    out << "Types:\n";
    for (const auto& cur : types) {
        out << "\t" << *cur.second << "\n";
    }

isSubtypeOf() [2/3]

static TypeConstraint souffle::ast::analysis::isSubtypeOf ( const TypeVar &  a, const TypeVar &  b  )

static

A constraint factory ensuring that all the types associated to the variable a are subtypes of the variable b.

Definition at line 27 of file TypeConstraints.cpp.

                                                                             {

Referenced by souffle::ast::analysis::TypeEnvironment::print(), and souffle::ast::analysis::TypeConstraintsAnalysis::visitNegation().

isSubtypeOf() [3/3]

static TypeConstraint souffle::ast::analysis::isSubtypeOf ( const TypeVar &  variable, const Type &  type  )

static

A constraint factory ensuring that all the types associated to the variable a are subtypes of type b.

Definition at line 35 of file TypeConstraints.cpp.

                                              : variable(std::move(variable)), type(type) {}
 
        bool update(Assignment<TypeVar>& assignments) const override {
            TypeSet& assignment = assignments[variable];
 
            if (assignment.isAll()) {
                assignment = TypeSet(type);
                return true;
            }
 
            TypeSet newAssignment;
            for (const Type& t : assignment) {
                newAssignment.insert(getGreatestCommonSubtypes(t, type));
            }
 
            // check whether there was a change
            if (assignment == newAssignment) {
                return false;
            }
            assignment = newAssignment;
            return true;
        }
 
        void print(std::ostream& out) const override {
            out << variable << " <: " << type.getName();
        }
    };
 
    return std::make_shared<C>(variable, type);
}
 
/**
 * A constraint factory ensuring that all the types associated to the variable
 * are subtypes of some type in the provided set (values)

isSubtypeOfComponent()

static TypeConstraint souffle::ast::analysis::isSubtypeOfComponent ( const TypeVar &  elementVariable, const TypeVar &  recordVariable, size_t  index  )

static

Constraint on record type and its elements.

Definition at line 320 of file TypeConstraints.cpp.

                : elementVariable(std::move(elementVariable)), recordVariable(std::move(recordVariable)),
                  index(index) {}
 
        bool update(Assignment<TypeVar>& assignment) const override {
            // get list of types for b
            const TypeSet& recordTypes = assignment[recordVariable];
 
            // if it is (not yet) constrainted => skip
            if (recordTypes.isAll()) {
                return false;
            }
 
            // compute new types for element and record
            TypeSet newElementTypes;
            TypeSet newRecordTypes;
 
            for (const Type& type : recordTypes) {
                // A type must be either a record type or a subset of a record type
                if (!isOfKind(type, TypeAttribute::Record)) {
                    continue;
                }
 
                const auto& typeAsRecord = *as<RecordType>(type);
 
                // Wrong size => skip.
                if (typeAsRecord.getFields().size() <= index) {
                    continue;
                }
 
                // Valid type for record.
                newRecordTypes.insert(type);
 
                // and its corresponding field.
                newElementTypes.insert(*typeAsRecord.getFields()[index]);
            }
 
            // combine with current types assigned to element
            newElementTypes = getGreatestCommonSubtypes(assignment[elementVariable], newElementTypes);
 
            // update values
            bool changed = false;
            if (newRecordTypes != recordTypes) {
                assignment[recordVariable] = newRecordTypes;
                changed = true;
            }
 
            if (assignment[elementVariable] != newElementTypes) {
                assignment[elementVariable] = newElementTypes;
                changed = true;
            }
 
            return changed;
        }
 
        void print(std::ostream& out) const override {
            out << elementVariable << " <: " << recordVariable << "::" << index;
        }
    };
 
    return std::make_shared<C>(elementVariable, recordVariable, index);
}
 
void TypeConstraintsAnalysis::visitSink(const Atom& atom) {
    iterateOverAtom(atom, [&](const Argument& argument, const Type& attributeType) {
        if (isA<RecordType>(attributeType)) {

satisfiesOverload()

static TypeConstraint souffle::ast::analysis::satisfiesOverload ( const TypeEnvironment &  typeEnv, IntrinsicFunctors  overloads, TypeVar  result, std::vector< TypeVar >  args, bool  subtypeResult  )

static

Given a set of overloads, wait the list of candidates to reduce to one and then apply its constraints.

NOTE: subtypeResult implies that func <: overload-return-type, rather than func = overload-return-type. This is required for old type semantics. See #1296 and tests/semantic/type_system4

Definition at line 230 of file TypeConstraints.cpp.

                : typeEnv(typeEnv), overloads(std::move(overloads)), result(std::move(result)),
                  args(std::move(args)), subtypeResult(subtypeResult) {}
 
        bool update(Assignment<TypeVar>& assigment) const override {
            auto subtypesOf = [&](const TypeSet& src, TypeAttribute tyAttr) {
                auto& ty = typeEnv.getConstantType(tyAttr);
                return src.filter(TypeSet(true), [&](auto&& x) { return isSubtypeOf(x, ty); });
            };
 
            auto possible = [&](TypeAttribute ty, const TypeVar& var) {
                auto& curr = assigment[var];
                return curr.isAll() || any_of(curr, [&](auto&& t) { return getTypeAttribute(t) == ty; });
            };
 
            overloads = filterNot(std::move(overloads), [&](const IntrinsicFunctorInfo& x) -> bool {
                if (!x.variadic && args.size() != x.params.size()) return true;  // arity mismatch?
 
                for (size_t i = 0; i < args.size(); ++i) {
                    if (!possible(x.params[x.variadic ? 0 : i], args[i])) return true;
                }
 
                return !possible(x.result, result);
            });
 
            bool changed = false;
            auto newResult = [&]() -> std::optional<TypeSet> {
                if (0 == overloads.size()) return TypeSet();
                if (1 < overloads.size()) return {};
 
                auto& overload = overloads.front().get();
                // `ord` is freakin' magical: it has the signature `a -> Int`.
                // As a consequence, we might be given non-primitive arguments (i.e. types for which
                // `TypeEnv::getConstantType` is undefined).
                // Handle this by not imposing constraints on the arguments.
                if (overload.op != FunctorOp::ORD) {
                    for (size_t i = 0; i < args.size(); ++i) {
                        auto argTy = overload.params[overload.variadic ? 0 : i];
                        auto& currArg = assigment[args[i]];
                        auto newArg = subtypesOf(currArg, argTy);
                        changed |= currArg != newArg;
                        // 2020-05-09: CI linter says to remove `std::move`, but clang-tidy-10 is happy.
                        currArg = std::move(newArg);  // NOLINT
                    }
                }
 
                if (nonMonotonicUpdate || subtypeResult) {
                    return subtypesOf(assigment[result], overload.result);
                } else {
                    nonMonotonicUpdate = true;
                    return TypeSet{typeEnv.getConstantType(overload.result)};
                }
            }();
 
            if (newResult) {
                auto& curr = assigment[result];
                changed |= curr != *newResult;
                // 2020-05-09: CI linter says to remove `std::move`, but clang-tidy-10 is happy.
                curr = std::move(*newResult);  // NOLINT
            }
 
            return changed;
        }
 
        void print(std::ostream& out) const override {
            // TODO (darth_tytus): is this description correct?
            out << "∃ t : " << result << " <: t where t is a base type";
        }
    };
 
    return std::make_shared<C>(
            typeEnv, std::move(overloads), std::move(result), std::move(args), subtypeResult);
}
 
/**
 * Constraint on record type and its elements.
 */

Referenced by souffle::ast::analysis::TypeConstraintsAnalysis::visitFunctor().

sub() [1/2]

template<typename Var , typename Val = typename Var::property_space::value_type>

std::shared_ptr<Constraint<Var> > souffle::ast::analysis::sub	(	const Val &	a,
		const Var &	b,
		const std::string &	symbol = "⊑"
	)

A generic factory for constraints of the form.

                           a ⊑ b

where b is a variables, a is a value of b's property space, and ⊑ is the order relation induced by b's property space.

Definition at line 257 of file ConstraintSystem.h.

                                            : a(std::move(a)), b(std::move(b)), symbol(std::move(symbol)) {}
 
        bool update(Assignment<Var>& ass) const override {
            typename Var::property_space::meet_assign_op_type meet_assign;
            return meet_assign(ass[b], a);
        }
 
        void print(std::ostream& out) const override {
            out << a << " " << symbol << " " << b;
        }
    };
 
    return std::make_shared<Sub>(a, b, symbol);
}
 
//----------------------------------------------------------------------
//                           assignment
//----------------------------------------------------------------------
 
/**

sub() [2/2]

template<typename Var >

std::shared_ptr<Constraint<Var> > souffle::ast::analysis::sub	(	const Var &	a,
		const Var &	b,
		const std::string &	symbol = "⊑"
	)

A generic factory for constraints of the form.

                           a ⊑ b

where a and b are variables and ⊑ is the order relation induced by their associated property space.

Definition at line 228 of file ConstraintSystem.h.

                                                         {
            typename Var::property_space::meet_assign_op_type meet_assign;
            return meet_assign(ass[b], ass[a]);
        }
 
        void print(std::ostream& out) const override {
            out << a << " " << symbol << " " << b;
        }
    };
 
    return std::make_shared<Sub>(a, b, symbol);
}
 
/**
 * A generic factory for constraints of the form
 *
 *                                a ⊑ b
 *

References b.

Referenced by souffle::ram::Program::clone(), souffle::ram::Program::getChildNodes(), souffle::ram::Program::getRelations(), souffle::ram::Program::print(), souffle::ram::Program::Program(), and souffle::ast::transform::reduceSubstitution().

subtypesOfTheSameBaseType()

static TypeConstraint souffle::ast::analysis::subtypesOfTheSameBaseType ( const TypeVar &  left, const TypeVar &  right  )

static

Ensure that types of left and right have the same base types.

Definition at line 130 of file TypeConstraints.cpp.

                                       : left(std::move(left)), right(std::move(right)) {}
 
        bool update(Assignment<TypeVar>& assigment) const override {
            // get current value of variable a
            TypeSet& assigmentsLeft = assigment[left];
            TypeSet& assigmentsRight = assigment[right];
 
            // Base types common to left and right variables.
            TypeSet baseTypes;
 
            // Base types present in left/right variable.
            TypeSet baseTypesLeft;
            TypeSet baseTypesRight;
 
            // Iterate over possible types extracting base types.
            // Left
            if (!assigmentsLeft.isAll()) {
                for (const Type& type : assigmentsLeft) {
                    if (isA<SubsetType>(type) || isA<ConstantType>(type)) {
                        baseTypesLeft.insert(getBaseType(&type));
                    }
                }
            }
            // Right
            if (!assigmentsRight.isAll()) {
                for (const Type& type : assigmentsRight) {
                    if (isA<SubsetType>(type) || isA<ConstantType>(type)) {
                        baseTypesRight.insert(getBaseType(&type));
                    }
                }
            }
 
            TypeSet resultLeft;
            TypeSet resultRight;
 
            // Handle all
            if (assigmentsLeft.isAll() && assigmentsRight.isAll()) {
                return false;
            }
 
            // If left xor right is all, assign base types of the other side as possible values.
            if (assigmentsLeft.isAll()) {
                assigmentsLeft = baseTypesRight;
                return true;
            }
            if (assigmentsRight.isAll()) {
                assigmentsRight = baseTypesLeft;
                return true;
            }
 
            baseTypes = TypeSet::intersection(baseTypesLeft, baseTypesRight);
 
            // Allow types if they are subtypes of any of the common base types.
            for (const Type& type : assigmentsLeft) {
                bool isSubtypeOfCommonBaseType = any_of(baseTypes.begin(), baseTypes.end(),
                        [&type](const Type& baseType) { return isSubtypeOf(type, baseType); });
                if (isSubtypeOfCommonBaseType) {
                    resultLeft.insert(type);
                }
            }
 
            for (const Type& type : assigmentsRight) {
                bool isSubtypeOfCommonBaseType = any_of(baseTypes.begin(), baseTypes.end(),
                        [&type](const Type& baseType) { return isSubtypeOf(type, baseType); });
                if (isSubtypeOfCommonBaseType) {
                    resultRight.insert(type);
                }
            }
 
            // check whether there was a change
            if (resultLeft == assigmentsLeft && resultRight == assigmentsRight) {
                return false;
            }
            assigmentsLeft = resultLeft;
            assigmentsRight = resultRight;
            return true;
        }
        //
        void print(std::ostream& out) const override {
            out << "∃ t : (" << left << " <: t)"
                << " ∧ "
                << "(" << right << " <: t)"
                << " where t is a base type";
        }
    };
 
    return std::make_shared<C>(left, right);
}
 
/**
 * Given a set of overloads, wait the list of candidates to reduce to one and then apply its constraints.
 * NOTE:  `subtypeResult` implies that `func <: overload-return-type`, rather than

Referenced by souffle::ast::analysis::TypeConstraintsAnalysis::visitFunctor().