Declarative program engine for large-scale program analysis

Patent metadata

Field	Value
Publication number	US-2016299748-A1
Application number	US-201514714208-A
Country	US
Kind code	A1
Filing date	May 15, 2015
Priority date	Apr 10, 2015
Publication date	Oct 13, 2016
Grant date	—

Abstract

A method and system for for staged compilation of a declarative program that includes receiving the declarative program, parsing and semantically checking the declarative program, translating the declarative program into a relational algebra machine (RAM) using a modified semi-naïve algorithm, performing a translation of the RAM into code of an imperative programming language to obtain a translated RAM, generating specialized extractor code in the imperative programming language, generating query application programming interface (API) code in the imperative programming language, and compiling the translated RAM, the specialized extractor code, and the query API code to obtain a program analysis module.

First claim

1 . A method for staged compilation of a declarative program comprising:
receiving the declarative program; parsing and semantically checking the declarative program; translating the declarative program into a relational algebra machine (RAM) using a modified semi-naïve algorithm, wherein the modified semi-naïve algorithm is a semi-naïve algorithm with modifications comprising unrolling two iterations of a fixed-point loop; performing a translation of the RAM into code of an imperative programming language to obtain a translated RAM; generating specialized extractor code in the imperative programming language; generating query application programming interface (API) code in the imperative programming language; and compiling the translated RAM, the specialized extractor code, and the query API code to obtain a program analysis module.

2 . The method of claim 1 , wherein, after compilation, the program analysis module comprises a program analysis engine, a specialized extractor, and a query API.

3 . The method of claim 2 , further comprising:
receiving a program for analysis; providing the program as input to the program analysis module; performing a static program analysis on the program; receiving, via the query API, a static program analysis query; and returning, in response to the static program analysis query, a static program analysis result comprising a security vulnerability of the program.

4 . The method of claim 3 , wherein performing the static program analysis comprises:
extracting, from the program, using the specialized extractor, a plurality of input relations; and performing, by the program analysis engine, using the plurality of input relations, the static program analysis.

5 . The method of claim 1 , wherein translating the declarative program into the RAM using the modified semi-naïve algorithm comprises:
performing a set of initial operations;
executing, after performing the set of initial operations, a plurality of first unrolled loop iterations;
making a first determination, after executing the plurality of first unrolled loop iterations, that first new knowledge was found during execution of the plurality of first unrolled loop iterations;
adding the first new knowledge to current knowledge to obtain first updated current knowledge;
executing, after executing the plurality of first unrolled loop iterations, a plurality of second unrolled loop iterations;
making a second determination, after executing the plurality of second unrolled loop iterations, that second new knowledge was found during execution of the plurality of second unrolled loop iterations;
adding the second new knowledge to the first updated current knowledge to obtain second updated current knowledge;
re-executing the plurality of first unrolled loop iterations and the plurality of second unrolled loop iterations until a third determination is made that no new knowledge is found after execution of one selected from a group consisting of the plurality first unrolled loop iterations and the plurality of second unrolled loop iterations; and
adding, based on the third determination, relations of a component to a computed relations set.

6 . The method of claim 5 , wherein each first unrolled loop iteration of the plurality of first unrolled loop iterations comprises:
initializing a Y knowledge by setting the Y knowledge to a Y knowledge empty set, selecting a rule of a plurality of rules of the relation of the component; performing a first evaluation of the relation using a relation current knowledge and the X knowledge to obtain a first evaluation result; and updating the Y knowledge using the first evaluation result; and wherein each second unrolled loop iteration of the plurality of second unrolled loop iterations comprises: initializing the X knowledge by setting the X knowledge to an X knowledge empty set; selecting the rule of the relation of the component; performing a second evaluation of the relation using the first updated current knowledge to obtain a second evaluation result; and updating relation X knowledge using the second evaluation result.

7 . The method of claim 1 , wherein the use of the modified semi-naïve algorithm enables parallelization of a plurality of operations.

8 . The method of claim 1 , wherein the declarative program is expressed in Datalog.

9 . A system for staged compilation of a declarative program comprising:
a declarative language compiler configured to receive a declarative program as input, and comprising:
a parse and semantic check module configured to parse and semantically check the declarative program;
a graph generation module configured to compute a strongly connected component graph;
a relational algebra machine (RAM) generation module configured to translate the declarative program into a relational algebra machine (RAM) using a modified semi-naïve algorithm, wherein the modified semi-naïve algorithm is a semi-naïve algorithm with modifications comprising unrolling two iterations of a fixed-point loop; and
a code generation module configured to:
perform a translation of the RAM into code of an imperative programming language to obtain a translated RAM;
generate specialized extractor code in the imperative programming language;
generate query API code in the imperative programming language; and
compile the translated RAM, the specialized extractor code, and the query API code to obtain a program analysis module.

10 . The system of claim 9 , wherein, after compilation, the program analysis module comprises a program analysis engine, a specialized extractor, and a query API.

11 . The system of claim 10 , wherein after compilation of the program analysis module, the program analysis module is configured to:
receive a program for analysis; perform a static program analysis on the program; receive, via the query API, a static program analysis query; return, in response to the static program analysis query, a static program analysis result comprising a security vulnerability of the program.

12 . The system of claim 9 , wherein use of the modified semi-naïve algorithm causes the RAM generation module to be configured to:
perform a set of initial operations;
execute, after performing the set of initial operations, a plurality of first unrolled loop iterations;
make a first determination, after executing the plurality of first unrolled loop iterations, that first new knowledge was found during execution of the plurality of first unrolled loop iterations;
add the first new knowledge to current knowledge to obtain first updated current knowledge;
execute, after executing the plurality of first unrolled loop iterations, a plurality of second unrolled loop iterations;
make a second determination, after executing the plurality of second unrolled loop iterations, that second new knowledge was found during execution of the plurality of second unrolled loop iterations;
add the second new knowledge to the first updated current knowledge to obtain second updated current knowledge;
re-execute the plurality of first unrolled loop iterations and the plurality of second unrolled loop iterations until a third determination is made that no new knowledge is found after execution of one selected from a group consisting of the plurality first unrolled loop iterations and the plurality of second unrolled loop iterations; and
add, based on the third determination, relations of a component to a computed relations set.

13 . A non-transitory computer readable medium comprising instructions that, when executed by a computer processor, perform a method for staged compilation

Assignees

• Oracle Int Corp

Inventors

• Scholz Bernhard F
• Westmann Till

Classifications

• G06F8/443

  Optimisation · CPC title

• G06F8/427 Primary

  Parsing · CPC title

• G06F8/436

  Semantic checking · CPC title