Verification of computer-executable code generated from a model

• US 9,612,806 B2
• Filed: 09/02/2014
• Issued: 04/04/2017
• Est. Priority Date: 10/06/2008
• Status: Active Grant

• Current Assignee: The MathWorks, Inc.
• Original Assignee: The MathWorks, Inc.
• Inventors: Conrad, Mirko, Lin, Xiaocang, Yan, Jun, Szpak, Peter S., Nirakh, Appa Rao, Shankar, Jayaprabha
• Primary Examiner(s): Kang, Insun
• Assistant Examiner(s): Lunar, Roberto E
• Application Number:
  US14/475,302
• Publication Number:
  US 20140380269A1
• Time in Patent Office: 945 Days
• Field of Search: None
• CPC Class Codes: G06F 11/3604 Software analysis for verifying properties of programs byte-code verification G06F9/44589
• CPC Class Codes: G06F 8/35 model driven

Abstract

In an embodiment, a model is sliced into a plurality of slices. A slice in the plurality of slices is selected. A portion of code, that corresponds to the selected slice, is identified from code generated from the model. The identified code is verified to be equivalent to the selected slice. Equivalence may include equivalent functionality, equivalent data types, equivalent performance, and or other forms of equivalence between the selected slice and the identified generated code.

Claims

1. One or more tangible non-transitory computer-readable storage media storing instructions, the instructions comprising:

one or more instructions that, when executed by one or more processors, cause the one or more processors to;

slice a model into a plurality of slices,

each slice, of the plurality of slices, including a different portion of the model;

select a slice from the plurality of slices;

generate a first intermediate representation based on the selected slice;

identify a portion of code, in code generated from the model, that corresponds to the selected slice;

generate a second intermediate representation based on the portion of code;

normalize the first intermediate representation and the second intermediate representation;

compare the normalized first intermediate representation with the normalized second intermediate representation; and

verify, based on the comparing the normalized first intermediate representation and the normalized second intermediate representation, whether the portion of code is equivalent to the selected slice.

2. The one or more tangible non-transitory computer-readable media of claim 1, where the instructions further comprise:

one or more instructions to detect, based on the comparing, a verification failure.

3. The one or more tangible non-transitory computer-readable media of claim 2, where the instructions further comprise:

one or more instructions to generate a report including information regarding the verification failure; and

one or more instructions to provide the report.

4. The one or more tangible non-transitory computer-readable media of claim 2, where the one or more instructions to detect the verification failure include:

one or more instructions to determine that the normalized second intermediate representation includes an element not corresponding with any element included in the normalized first intermediate representation.

5. The one or more tangible non-transitory computer-readable media of claim 1, where the instructions further comprise:

one or more instructions to select a second slice from the plurality of slices;

one or more instructions to generate a third intermediate representation based on the second selected slice;

one or more instructions to identify a second portion of code, in code generated from the model, that corresponds to the second selected slice;

one or more instructions to generate a fourth intermediate representation based on the second portion of code;

one or more instructions to normalize the third intermediate representation and the fourth intermediate representation;

one or more instructions to compare the normalized third intermediate representation with the normalized fourth intermediate representation; and

one or more instructions to verify, based on the comparing the normalized third intermediate representation and the normalized fourth intermediate representation, whether the second portion of code is equivalent to the second selected slice.

6. The one or more tangible non-transitory computer-readable media of claim 1, where the one or more instructions to generate the first intermediate representation include:

one or more instructions to generate an element connectivity list based on the selected slice.

7. The one or more tangible non-transitory computer-readable media of claim 1, where the one or more instructions to generate the second intermediate representation include:

one or more instructions to generate an abstract syntax tree based on the portion of code.

8. The one or more tangible non-transitory computer-readable media of claim 1, where

the instructions further comprise:

one or more instructions to generate a program dependency intermediate representation based on one or more data dependencies in the portion of the code and based on one or more control dependencies in the portion of the code, and

the one or more instructions to slice the model include;

one or more instructions to slice the program dependency intermediate representation into the plurality of slices.

9. The one or more tangible non-transitory computer-readable media of claim 8, where the program dependency intermediate representation includes a graph G(e, v),

where e represents one or more edges and v represents a plurality of vertices, and

where the one or more instructions to slice the program dependency intermediate representation include:

one or more instructions to slice the program dependency intermediate representation based on determining that given a vertex v_i, of the plurality of vertices of the graph G(e, v), a slice of graph G(e, v), with respect to v_i, is a graph G′

(e′

, v′

) that contains one or more vertices, of the plurality of vertices, of which v_i has a transitive flow or a control dependency.

10. The one or more tangible non-transitory computer-readable media of claim 1, where

the one or more instructions to generate the second intermediate representation include:

one or more instructions to generate a program dependency graph based on the portion of code, and

the one or more instructions to normalize the first intermediate representation and the second intermediate representation include;

one or more instructions to normalize the program dependency graph.

11. The one or more tangible non-transitory computer-readable media of claim 1, where

the portion of code contains a statement,

the instructions further comprise:

one or more instructions to identify a semantic equivalent for the statement in the portion of code; and

one or more instructions to replace the statement in the portion of code with the identified semantic equivalent, and

the one or more instructions to generate the second intermediate representation include;

one or more instructions to generate the second intermediate representation based on replacing the statement with the semantic equivalent.

12. The one or more tangible non-transitory computer-readable media of claim 1, where

the portion of code contains a plurality of statements,

the instructions further comprise:

one or more instructions to replace the plurality of statements in the portion of code with a phi node,

the phi node representing at least one of;

a control flow of the replaced plurality of statements, or

a data flow of the replaced plurality of statements, and

the one or more instructions to generate the second intermediate representation include;

one or more instructions to generate the second intermediate representation based on replacing the plurality of statements with the phi node.

13. The one or more tangible non-transitory computer-readable media of claim 1, where the instructions further comprise:

one or more instructions to perform a transformation operation on the second intermediate representation; and

one or more instructions to provide a result of the transformation operation performed on the second intermediate representation,

the result including information related to a change made to the second intermediate representation based on performing the transformation operation on the second intermediate representation.

14. The one or more tangible non-transitory computer-readable media of claim 1, where the instructions further comprise:

one or more instructions to identify an element in the selected slice for which corresponding code in the generated code cannot be identified; and

one or more instructions to separate the element from the selected slice for separate verification.

15. The one or more tangible non-transitory computer-readable media of claim 1, where the instructions further comprise:

one or more instructions to indicate, in a block diagram display of the model, that a portion of the model, included in the selected slice, is unverifiable.

16. The one or more tangible non-transitory computer-readable media of claim 1, where the instructions further comprise:

one or more instructions to identify an element in the selected slice which cannot be verified; and

one or more instructions to modify the identified element to make the identified element verifiable.

17. The one or more tangible non-transitory computer-readable media of claim 1, where the one or more instructions to verify whether the portion of code is equivalent to the selected slice include:

one or more instructions to verify whether the portion of code is equivalent to the selected slice independent of verifying another slice, of the plurality of slices, is equivalent to another portion of code.

18. The one or more tangible non-transitory computer-readable media of claim 17, where the other slice is unverifiable.

19. The one or more tangible non-transitory computer-readable media of claim 17, where the instructions further comprise:

one or more instructions to verify the other slice is equivalent to the other portion of code based on a manual verification.

20. A method comprising:

selecting a slice of a model from a plurality of slices of the model,

the plurality of slices of the model being identified based on one or more criteria, and

the selecting the slice being performed by a device;

identifying a portion of code, in code generated for the model, that corresponds to the slice,

the identifying the portion of code being performed by the device;

generating an intermediate representation (IR) of the slice of the model,

the generating the IR of the slice being performed by the device;

generating an IR of the portion of code,

the generating the IR of the portion of the code being performed by the device;

normalizing the IR of the slice and the IR of the portion of the code,

the normalizing the IR of the slice and the IR of the portion of code being performed by the device;

comparing the normalized IR of the slice with the normalized IR of the portion of code,

the comparing the normalized IR of the slice with the normalized IR of the portion of code being performed by the device; and

verifying, based on the comparing the normalized IR of the slice and the normalized IR of the portion of code, whether the portion of code is equivalent to the slice,

the verifying whether the slice is equivalent to the portion of code being performed by the device.

21. The method of claim 20, where

the portion of code includes one or more data dependencies and one or more control dependencies, and

generating the IR of the portion of code includes:

generating a program dependency graph that represents the one or more data dependencies and the one or more control dependencies; and

slicing the program dependency graph,

where the program dependency graph includes a graph G(e, v),

where e represents one or more edges and v represents a plurality of vertices, and

where the program dependency graph is sliced based on;

 

given a vertex v_i of the graph G(e, v), a slice, of the plurality of slices of graph G(e, v), with respect to v_i is a graph G′

(e′

, v′

) containing one or more vertices, of the plurality of vertices, of which v_i has a transitive flow or a control dependency.

22. The method of claim 21, where

generating the IR of the portion of the code includes:

performing a transformation on the IR of the portion of the code, and

the method further comprises;

outputting information identifying a change made to the IR of the portion of the code,

the change being made to the IR of the portion of the code based on performing the transformation on the IR of the portion of the code.

23. The method of claim 20, where verifying whether the portion of code is equivalent to the slice includes:

verifying whether the portion of code is equivalent to the slice independent of verifying another slice, of the plurality of slices, is equivalent to another portion of code.

24. The method of claim 23, where the other slice is unverifiable.

25. The method of claim 23, where the method further comprises:

verifying the other slice is equivalent to the other portion of code based on a manual verification.

26. A device comprising:

one or more processors, implemented at least partially in hardware, to;

slice a model into a plurality of slices,

each slice, of the plurality of slices, including a different portion of the model;

select a slice from the plurality of slices;

generate a first intermediate representation based on the selected slice;

identify a portion of code, in code generated from the model, that corresponds to the selected slice;

generate a second intermediate representation based on the portion of code;

normalize the first intermediate representation and the second intermediate representation;

compare the normalized first intermediate representation with the normalized second intermediate representation; and

verify, based on the comparing the normalized first intermediate representation and the normalized second intermediate representation, whether the portion of code is equivalent to the selected slice.

27. The device of claim 26, where the one or more processors, when verifying whether the portion of code is equivalent to the selected slice, are to:

verify whether the portion of code is equivalent to the selected slice independent of verifying another slice, of the plurality of slices, is equivalent to another portion of code.

28. The device of claim 27, where the other slice is unverifiable.

29. The device of claim 27, where the one or more processors are further to:

verify the other slice is equivalent to the other portion of code based on a manual verification.