K-user mailing list

["Moore, Brandon Michael" <bmmoore AT illinois.edu>]

We don't have conditions like "Res = addMInt(RdV, RrV)" at the moment, but it's something we'd like to do eventually.

For now, you can handle that sort of thing with an extra computational step.

In the general case you can just make a bit of syntax to hold intermediate results, without looking at all what anything means.

syntax KItem ::= added(Reg,MInt,MInt,MInt)

If it's in your semantics module (or anything but the syntax module) it won't mess up parsing of programs, but you can still use it in rules:

rule <k>add Rd , Rr => added(Rd,RdV,RrV,addMInt(RdV,RrV)) ...</k>
     <registers>... (Rr |-> RrV) (Rd |-> RdV) ...</registers>
rule <k>added(Rd,RdV,RrV,Res) => .</k>
     <registers>... Rd |-> _ => Res ...</registers>        <rh> _ => addrh(bit(RdV, 3), bit(RrV, 3), bit(addMInt(RdV, RrV), 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>

If your operations are more organized and some instructions share behavior, you might want to break rules down into smaller steps, so the added label are meaningful and reusable. Hopefully this is reasonable for your processor:

syntax KItem ::= store(Reg,MInt) | setOverflowFlags(MInt,MInt,MInt) | setResultFlags(MInt) | tick

rule <k>add Rd , Rv =>
  store(Rd, addMInt(RdV,RvV)) ~>
  setOverflowFlags(RdV, RvV, addMInt(RdV,RvV)) ~>
  setResultFlags(addMInt(RdV,RvV)) ~>
  tick 
  ...</k>

rule <k>store(R,V) => . ...</k><registers>... R |-> _ => V ...</registers>
rule <k>setResultFlags(Res) =>. ...</k>      

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

        <rz> _ => eqMInt(Res, toByte(0)) </rz>
rule <k>setResultFlags(V1,V2,Res) => . ...</k>

        <rh> _ => addrh(bit(V1, 3), bit(V2, 3), bit(Res, 3)) </rh>

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

        <rv> _ => addrv(bit(V1, 7), bit(V2, 7), bit(Res, 7)) </rv>

        <rc> _ => overflowMInt(uaddMInt(V1, V2)) </rc>       

rule <k>tick => . ...</k><clockcycle> C => C +Int 1 </clockcycle>

This reminds me a bit even of how the flags might be defined in a hardware description language, except for our ~> being more sequential. I don't know your processor and didn't follow the details of your boolean expressions but you could probably share that "setResultFlags" with several operations, and "setOverflowFlags" at least with subtraction (or fix them up to better suite your processor, of course).

If you worry the granularity is too fine, there are ways to label rules and make the stepper stop only after ones you care about (maybe just after every "tick"), which I won't go into here.

Naming and separating small operations like that may make the duplication more tolerable. If not, you can combine approaches until K has a way to name intermediate results:

rule <k>add Rd , Rr => added(Rd,RdV,RrV,addMInt(RdV,RrV)) ...</k>
     <registers>... (Rr |-> RrV) (Rd |-> RdV) ...</registers>
rule <k>added(Rd,V1,V2,Res) =>
  store(Rd, Res) ~>
  setOverflowFlags(V1, V2, Res) ~>
  setResultFlags(Res) ~>
  tick 
  ...</k>

Brandon

---

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Frederico Zica [fredzica AT gmail.com]
Sent: Wednesday, July 30, 2014 7:42 PM
To: k-user AT cs.uiuc.edu
Subject: [K-user] Repeating expressions in a rewrite rule

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