K-user mailing list

[Frederico Zica <fredzica AT gmail.com>]

Hello.

I'm using the K to define the semantics of a assembly language of an 8-bits microcontroller family.

Some of the language assembly instructions interfere in the values of the SREG - the status register of the microcontroller. In my case it's represented as 8 configuration cells:  

<sreg>
     <ri> false </ri>
     <rt> false </rt>
     <rh> false </rh>
     <rs> false </rs>
     <rv> false </rv>
     <rn> false </rn>
     <rz> false </rz>
     <rc> false </rc>
</sreg>

My problem is that many of the instructions require the same operations to be done in different cells, and hence I have duplicate code. As an example I'll have the code of the add operation here below.

    rule <k> add Rd, Rr => . </k>

        <registers>... (Rr |-> RrV) (Rd |-> (RdV => addMInt(RdV, RrV)))  ...</registers>

        <rh> _ => addrh(bit(RdV, 3), bit(RrV, 3), bit(addMInt(RdV, RrV), 3)) </rh>

        <rs> _ => addrv(bit(RdV, 7), bit(RrV, 7), bit(addMInt(RdV, RrV), 7)) xorBool bit(addMInt(RdV, RrV), 7) </rs> // V⊕ N for signed tests  

        <rv> _ => addrv(bit(RdV, 7), bit(RrV, 7), bit(addMInt(RdV, RrV), 7)) </rv>

        <rn> _ => bit(addMInt(RdV, RrV), 7) </rn>

        <rz> _ => eqMInt(addMInt(RdV, RrV), toByte(0)) </rz>

        <rc> _ => overflowMInt(uaddMInt(RdV, RrV)) </rc>

        <clockcycle> C => C +Int 1 </clockcycle>

     // Add flags

     syntax Bool ::= addrv(Bool, Bool, Bool) [function]

     syntax Bool ::= addrh(Bool, Bool, Bool) [function]    

 

     // Rd7 • Rr7 • R7 ¯ + Rd7 ¯ • Rr7 ¯ • R7

     rule addrv(Rd7b, Rr7b, R7b) =>

         Rd7b andBool

         Rr7b andBool

         (notBool R7b) orBool

         (notBool Rd7b) andBool

         (notBool Rr7b) andBool

         R7b [macro]

 

     // Rd3 • Rr3 + Rr3 • R3 ¯ + R3 ¯ • Rd3

     rule addrh(Rd3b, Rr3b, R3b) =>

         Rd3b andBool

         Rr3b orBool

         Rr3b andBool

         (notBool R3b) orBool

         (notBool R3b) andBool

         Rd3b [macro]

You can see that some function calls are repeated many times, for instance the 'addMInt(RdV, RrV)'. I know that I could use macro definitions to centralize each of the repeating piece of code, exactly as I did with 'addrv' and 'addrh', but I don't see it as a very good decision because that would create a macro that will be used only in one rewrite rule and it would still compute the values many times. I can imagine a 'where' clause that could facilitate this task, in which I would be able to name a variable, like this:

    rule <k> add Rd, Rr => . </k>

        <registers>... (Rr |-> RrV) (Rd |-> (RdV => Res))  ...</registers>

        <rh> _ => addrh(bit(RdV, 3), bit(RrV, 3), bit(Res, 3)) </rh>

        <rs> _ => addrv(bit(RdV, 7), bit(RrV, 7), bit(Res, 7)) xorBool bit(Res, 7) </rs> // V⊕ N for signed tests  

        <rv> _ => addrv(bit(RdV, 7), bit(RrV, 7), bit(Res, 7)) </rv>

        <rn> _ => bit(Res, 7) </rn>

        <rz> _ => eqMInt(Res, toByte(0)) </rz>

        <rc> _ => overflowMInt(uaddMInt(RdV, RrV)) </rc>

        <clockcycle> C => C +Int 1 </clockcycle>

        where Res = addMInt(RdV, RrV)

Is there a functionality like this in K? Can I do it somehow?

Thanks,

Frederico Zica