the Judgement of the Equivalence of Programs

Introduction

This is a program equivalence verification tool.

• Automatically judge whether two programs are equivalent.
• Provide interface for interactive confirmation.
• This tool have been tested, including unit test and performance test.

Background

The existing tool eqminer can generate several code blocks (each code block is packaged as a function) according to a given source program, and cluster them into several cIuster by dynamically executing these functions, and the functions in each cIuster are considered to be equivalent to each other. Eqminer's principle of judging equivalence is to compare whether two programs have the same output when they have the same input. Obviously, all the functions in cIuster generated by dynamic execution are not necessarily completely equivalent to each other, because the process of dynamic execution is endless. At this time, manual confirmation is needed to ensure its equivalence.

How to judge

All the input values of the function are randomly generated and independent of each other. When judging equivalence, the number of inputs (or outputs) of two functions can be different, and the order can also be different. Both input and output are regarded as the concept of set, and whether the set of output values presents an inclusive relationship when two functions have the same input is compared. If the inclusion relation is presented, the two are equivalent, otherwise they are not equivalent.

When the number of inputs is different (for example, one is I, one is J, and i<j), the same input means that two functions have the same I inputs, and the function with the number of inputs J will have additional j-i randomly generated inputs.

Input value is also the concept of set, and the same variable name in two functions does not necessarily have the same input value.

For more, please refer to manual.pdf

How to use

You can provide a set of data, and each set of data contains several folders (each folder is a cIuster).

For each folder (which contains n files), this tool will judge the equivalence of any two files and record them in csv file. If it is equivalent, it will be recorded in groupID-equaI-pairs.csv; If it is not equivalent, it will be recorded in groupid-inequai-pairs.csv.

The total amount of data generated by each folder (including equivalence and non-equivalence) should be $C_n^2$. In the case of no duplicate data. The handling of duplicate data will be mentioned below.

Snapshots

• Log in

  

• Automatic Judgement

• Manual Judgement && "Diff" Function