K Java Backend Simulation Tool

Introduction: The K simulation tool can check the trace simulation relation between two programs in two semantics. Traditional trace simulation relation compare whether or not all traces generated from one program have instances in the other program. Usually, the two programs are in the same semantics. Now, the k simulation tool makes a further progress. We can allow the users to define the two programs in two different semantics.

relation: The trace simulation will answer true or false, and it is the answer for the following relation:

for programa p, programb q in semantics a and b

let -a-> represent a step move in a program, then for every next steps p' of programa, and its corresponding predicate b and the expression a generated by this step, there exists a program q', and its corresponding predicate b', and expression a', such that

p -a-> (b,p) and q -a'-> (b',q')

and expression a is satisfiable under predicate b, and expression a' is satisfiable under predicate b', and the formula (for_all x, (x=a) /\ (x=a') /\ b => b') is satisfiable

Command: Before users are able to run the simulation tools, users need to create two compiled semantic files in two different directory. For example, if users want to compile a imp.k file. They can run the following command:

kompile --backend java -d directory_name imp.k

After users have finished the two semantic files (they can be one semantics in one directory), users can use the following commands to run the simulation checking:

krun --backend java --simulation="directorya directoryb programa programb" krun --backend java --smt none --simulation="directorya directoryb programa programb"

The programa corresponds to a program under the syntax and semantics defined by the file in directorya, while the programb corresponds to a program under the syntax and semantics defined by the file in directoryb. The command will answer true or false.

The command without setting smt to none means that the users can suggest that they care about one content of a cell, but what they care can be expressions (with variables), and the simulation tool is able to match all assignments for the expressions. If the users use the command with smt setting to none, it means that the users assume that all they care in every step are values (without variables). In this case, the simulation tool will compare the two values from two programs and see if they are equal.

They users can provide what they care about in evaluating the programs. This can be done by a special rule attribute "alphaRule". Due to the parsing problem, current the rule needs to associate with an anywhere attribute. the users can write the following rule in their semantics file: rule ...... [anywhere,alphaRule]

We will assume that each semantics file only has one such rule. If users do not provide this rule, we will assume that users do not care about any content. Thus, we will check whether or not for every paths from the first program, there is a corresponding path in the second program associated with it.

Example:

Let's define a imp.k file as usual, but we have the following configuration and two different rules:

imp.k configuration $PGM:Stmts // $PGM:K .Map 0 0 .Map .List .List ... rule X:Id = I:Int => I ... ... X |-> L:KItem ... I':Int => I ... L |-> (_:KItem => I) ... [assignment,transition] ... rule ( T TH I:Int ) => I [anywhere,alphaRule] ...

The imp.k contains an extra cell called simulation (for simplicity, users could avoid defining this cell).. The assignment rule will put values into the simulation cell, while the alphaRule will select the simulation cell in each step evluation, then the user suggests that he cares about the simulation cell.

Then we use the commands: kompile --backend java -d a imp.k kompile --backend java -d b imp.k

These two commands will compile the imp.k into two different directory, and we wrong the following two programs:

assignment_1: int X ; X = 1 ; X = 3 ; X = 3 ; X = 3 ;

assignment_2: int Y ; Y = 1 ; Y = 2 ; Y = 3 ; Y = 3 ;

Then, after the user type in the command: krun --backend java simulation="a b assignment_1 assignment_2", the simulation tool in K will answer false, because in the third step, the user cared content of assignment_2 is 2, while the user cared content of assignment_1 is 1. but if we fix the assignment_2 to be: int Y ; Y = 1 ; Y = 2 + 1 ; Y = 3 ; Y = 3 ;

Then the simulation tool will answer true. One can easily verify that if they use the command: krun --backend java --smt none simulation="a b assignment_1 assignment_2", they will get the same result.