Type inference for datalog with complex type hierarchies

Patent metadata

Field	Value
Publication number	US-RE46380-E
Application number	US-201514952788-A
Country	US
Kind code	E1
Filing date	Nov 25, 2015
Priority date	Jul 15, 2010
Publication date	Apr 25, 2017
Grant date	Apr 25, 2017

Abstract

What is disclosed are a novel system and method for inferring types of database queries. In one embodiment a program and associated database schema that includes a type hierarchy is accessed. The program includes query operations to a database that contains relations described by a database schema. Types are inferred from definitions in the program by replacing each database relationship in the program by the types in the database schema. A new program is generated with the types that have been inferred with the new program only accessing unary relations in the database. In another embodiment, testing of each of the types that have been inferred is performed for type emptiness. In response to type emptiness being found for a type that have been inferred, a variety of different operations are performing including removing the type, providing a notification regarding the emptiness found for the type, and more.

First claim

What is claimed is:

1. A computer-implemented method comprising:
accessing a query program with, the query program containing one or more queries to a database that contains relations described by at least one a database schema, wherein the database schema specifies a column type for every column of every extensional predicate that occurs in the query program;
receiving the database schema and at least one an entity type hierarchy for the database; and
inferring a first type program from definitions in the query program by replacing each use of a database relation an extensional predicate in the query program by its type in the conjunction of the column types of the columns of the extensional predicate, the column types being provided by the database schema, and the wherein each column type is at least portion of a respective second type program,
wherein each of the first type program and the second type program is a derived program using type symbols without other extensional relation symbols, and each of the first type program and the second type program do not contain negation,
wherein the first type program and the second type program uses programs use only extensionals that are monadic extensions, and the first type program and the second type programs do not contain negation;
testing portion portions of the first type program that has been inferred for type emptiness and type inclusion; and
finding type emptiness or type inclusion for a first portion of the first type program, wherein the first portion is also a type program; and
providing at least one of error information and or optimization information regarding the type emptiness and or type inclusion being found for the type first portion of the first type program.

2. The computer-implemented method of claim 1 , further comprising:
in response to type emptiness being found for a the first portion of the first type program that has been inferred during determining of the testing portion of portions of the first type program, performing at least one of:
removing the a type test from the query program a first portion of the query program that corresponds to the first portion of the first type program;
providing a notification regarding the emptiness found for the first portion of the first type program; or
providing notification on combining queries in the query program by conjunction without creating empty parts in a combined query;

in response to an empty part of a query being a conjunction, finding a smallest set of query parts that has a conjunction that is empty;
in response to a search for a smallest empty part of a database query that traverses all parts of the database query, pushing a conjunction of an approximation of the smallest empty part and a context on top of a stack of approximations of all contexts where the empty part is being used; and
eliminating empty query parts to achieve virtual method resolution in an object-oriented query language.

3. The computer-implemented method of claim 1 , further comprising:
in response to type inclusion being found for a second portion of the first type program that has been inferred during determining of the testing portion of portions of the first type program, performing at least one of:
removing the a type test from the query program a second portion of the query program that corresponds to the second portion of the first type program; and or
providing a notification regarding the type inclusion being found for the second portion of the first type program.

4. The computer-implemented method of claim 1 , further comprising wherein:
inferring the first type program includes inferring an inferred type for an intensional predicate in the query program that has a declared type in the query program; and
the method further comprises:
testing the type program that has been inferred for whether a database query is contained in a given portion of the type program; and in response to the database query not being contained in the given portion, performing at least one of:
removing a type test; and
determining that the inferred type does not contain the declared type; and
providing a notification regarding that the database query declared type is not being contained in the given portion inferred type.

5. The computer-implemented method of claim 1 , wherein portions of the first type program that has been inferred are represented by a set respective sets of type tuple constraints (TTCs), wherein each of the TTCs includes:
a tuple of type propositions;
an equivalence relation between tuple components, each tuple component being a type proposition; and
a set of inhabitation constraints.

6. The computer-implemented method of claim 5 , further comprising:
checking inclusion of a third portion of the first type program that has been inferred represented by a first set of TTCs into another, fourth portion of the first type program represented by a second set of TTCs by:
computing a set of prime implicants of the second set; and

checking each TTC in the first set and finding determining whether a larger TTC exists in the set of prime implicants of the second set of TTCs; and
determining that the third portion is included in the fourth portion if for each TTC in the first set a larger TTC exists in the set of prime implicants of the second set of TTCs.

7. The computer-implemented method of claim 6 , further comprising:
computing the set of prime implicants of the second set of TTCs by saturating the second set by exhaustively applying consensus operations to ensure all relevant TTCs are included.

8. The computer-implemented method of claim 7 , wherein each of the consensus operations are performed by includes generating a new TTC from two existing TTCs by
receiving two TTCs as operands two TTCs, the tuple of type propositions of each TTC having the same number of type propositions;
receiving a set of indices and, each index in the set identifying a type proposition in a tuple of type propositions by the position of the type proposition in the tuple;
equating in each operand TTC all columns whose indices type propositions at index positions that occur in the set of indices, and preserving all other equalities and inhabitation constraints of the operands each TTC operand, and then for each index position taking disjunctions over columns type propositions indexed in the set of indices and conjunctions over all other columns type propositions as the type propositions of the tuple of type propositions of the new TTC; and
takinggenerating a union of two or more of the equivalence relations in of the operands operand TTCs as the equivalence relation between tuple components of the new TTC; and
generating a pointwise disjunction of the inhabitation constraints of the operandsoperand TTCs as the inhabitation constraints of the new TTC.

9. The computer-implemented method of claim 8 , further comprising:
reducing a number of consensus operations that need to be performed during saturation by omitting consensus operations where a resulting TTC will be covered by TTCs already present in the set, wherein a TTC τ is covered by a TTC τ′ if τ<:τ′.

10. The computer-implemented method of claim 8 , further comprising:
receiving a logical formula that represents a type hierarchy, and representing a component type proposition of a TTC as a binary decision diagram (BDDs BDD), and choosing a BDD variable order by assigning neighboring indices of the set of indices to type symbols that appear in a same conjunct of the logical formula that represents the type hierarchy.

11. The computer-implemented method of claim 1 , wherein further comprising:
using the first type prog

Assignees

• Semmle Ltd

Inventors

• Schaefer Max
• De Moor Oege

Classifications

• G06F17/30421 Primary

  Physics · mapped topic

• G06F8/437 Primary

  Type checking · CPC title

• G06F16/2448

  for particular applications; for extensibility, e.g. user defined types · CPC title