Re: [PATCH] pickles: add pickle for RISC-V RV32I instruction set

[Jose E. Marchesi]

> Hi Jose.
>
> On Mon, Sep 12, 2022 at 11:11:59AM +0200, Jose E. Marchesi wrote:
>> 
>> > One important note, all instructions have four methods:
>> >   - as_asm
>> >   - as_poke
>> >   - _format
>> >   - _print
>> >
>> > `as_asm` and `as_poke` are super-useful in generating test cases.
>> 
>> That's nice.  I should add these to bpf.pk as well.  In fact, if we can
>> come with a nice convention for all pickles implementing instruction
>> sets, then we could write generic test tools.
>
>
> Yes, good idea.
>
>
>> 
>> Regarding _format, I suppose the intention is to have them behave like
>> _print right?  I like the idea, and a patch having the codegen calling
>> _format if it exists is welcome.
>> 
>
>
> Good :)
> I'll remove `_format`s until we improve the codegen.
>
>
>> 
>> Since `j' is only used in the `for' look, why not moving its declaration
>> there?  Something like:
>> 
>>   fun tcase_addi = RV32_Insn[]:
>>   {
>>     var insns = RV32_Insn[] ();
>> 
>>     for (var i = -2048, j = 0 as RV_Reg; i < 2048; ++i)
>>       apush (insns, rv32_addi (j, ++j, i));
>>     return insns;
>>   }
>> 
>
>
> Right.
>
>
>> > +// module riscv;
>> > +// push_endian (ENDIAN_LITTLE);
>> 
>> We don't support any of these (yet) :)
>> 
>
>
> Yes! I was just imagining a better world :D
>
>
>> > +set_endian (ENDIAN_LITTLE);
>> 
>> I don't think it is a good ideas for pickles to change the current
>> endianness when loaded.  Do any of the code in riscv.pk rely in
>> endianness _at load time_?
>> 
>
>
> No.
> But I'll comment it as a hint for the reader.
>
>
>> > +
>> > +/* Don't use standard types like bit, int, long, ... in order to make
>> > + * this pickle usable in gdb.
>> > + */
>> 
>> Good point.  I wonder if we should add a chapter on writing pickles for
>> instruction sets and document this?  Same applies to the as_asm and
>> as_poke methods.
>> 
>
>
> I think it's a good idea. The more uniform pickles, the better.
>
>
>> > +var RV32_OPCODE_BRANCH   = 0b1100011 as RV_Opcode,
>> > +    RV32_OPCODE_LOAD     = 0b0000011 as RV_Opcode,
>> > +    RV32_OPCODE_STORE    = 0b0100011 as RV_Opcode,
>> > +    RV32_OPCODE_SYSTEM   = 0b1110011 as RV_Opcode,
>> > +    RV32_OPCODE_OP_IMM   = 0b0010011 as RV_Opcode,
>> > +    RV32_OPCODE_OP       = 0b0110011 as RV_Opcode,
>> > +    RV32_OPCODE_MISC_MEM = 0b0001111 as RV_Opcode;
>> 
>> Hm, are these casts really necessary?
>> 
>
>
> Not really. But I wanted to use the right type for them.

Ok, I was just curious.

>> > +    var _name = [
>> > +      .[0b000] = funct7 ? "sub" : "add",
>> > +      .[0b001] = "sll",
>> > +      .[0b010] = "slt",
>> > +      .[0b011] = "sltu",
>> > +      .[0b100] = "xor",
>> > +      .[0b101] = funct7 ? "sra" : "srl",
>> > +      .[0b110] = "or",
>> > +      .[0b111] = "and",
>> > +    ];
>> 
>> Very nice this _name variable.  But why are you using a prefix
>> underscore?  Variables declared within types are not visible outside of
>> the type, and you don't have any field named `name'.
>> 
>
>
> Yes, I know it's not visible to user, but I just wanted to a visual 
> distinction
> for field names and variables. Maybe I'm over-thinking here :)
>
>> > +      {
>> > +        uint<1> i; // input
>> > +        uint<1> o; // output
>> > +        uint<1> r; // read
>> > +        uint<1> w; // write
>> 
>> Why not calling these fields `input', `output', `read' and `write' and
>> get rid of these comments?
>> 
>
>
> OK :)
> (You know I love short identifiers even when they're cryptic :D)

:)

>> > +    var ok = lambda int<32>:
>> > +      {
>> > +        if (opcode == RV32_OPCODE_JALR)
>> > +          assert (funct3 == 0);
>> > +        else if (opcode == RV32_OPCODE_LOAD)
>> > +          {
>> > +            assert (imm as _FenceNibble, "Predecessor set cannot be 
>> > empty");
>> > +            assert ((imm as uint<8> .>> 4) as _FenceNibble,
>> > +                    "Successor set cannot be empty");
>> 
>> I don't understand these conditions in the assertions.  What are they
>> for?
>> 
>> > +          }
>> > +        return 1; /* Dummy!  */
>> > +      }();
>> 
>> So you are using this variable `ok' just to trigger the execution of the
>> initializer?  Woulnd't be better to use field constraints instead?  Then
>> you wouldn't need any `Dummy!' stuff.
>> 
>> Also, I don't think it is OK for a pickle to raise an assertion because
>> of incorrect data.
>> 
>> What about something like this instead:
>> 
>>   RV_Opcode opcode : opcode in RV_OPCODES_I
>>                      && (opcode == RV_OPCODE_JALR => funct3 == 0)
>>                      && (opcode == RV32_OCODE_LOAD =>
>>                          imm as FenceNibble && (imm as uint<8> .>> 4) as 
>> FenceNibble);
>> 
>
>
> Oh, I completely forgot the awesome => operator!
>
> This is better and the intent is clear to Poke user :+1:
> And user can disable constraints, too (with assert approach it's not 
> possible).
>
> There's only one usability problem with this approach, when the constraint
> fails, user don't know which condition is false. I think we need a better
> message in constraint exceptions. E.g., something like
>   "constraint condition `opcode == RV_OPCODE_JALR => funct3 == 0` failed"
> WDYT?

I think it would be difficult to implement that reliably, because, at
what point of the expression do you cut?

It would be easier if we supported using several constraint
expressions, like in:

 RV_Opcode opcode : opcode in RV_OPCODES_I
                  : opcode == RV_OPCODE_JALR => funct3 == 0
                  : opcode == RV32_OCODE_LOAD =>
                     imm as FenceNibble && (imm as uint<8> .>> 4) as 
FenceNibble;

And actually that would match well with our existing intention of
supporting other "named" constraints, like:

 RV_Opcode opcode : opcode in RV_OPCODES_I
                  : opcode == RV_OPCODE_JALR => funct3 == 0
                  :warning opcode < 10;

Where : would be a synonym of :error.

> Or when can use (which is not ideal):
>
> ```poke
>   uint<8>[0] _cond0 : opcode == RV_OPCODE_JALR => funct3 == 0;
>   uint<8>[0] _cond1 : (opcode == RV32_OCODE_LOAD => imm as FenceNibble &&
>                         (imm as uint<8> .>> 4) as FenceNibble);
> ```

No I don't like that at all.

>> > +        if (opcode == RV32_OPCODE_FENCE)
>> > +          {
>> > +            assert (funct3 == 0); // because of RV32I
>> 
>> Move to a constraint?
>> 
>
>
> Yes.
>
>
>> > +
>> > +            var l = imm as _FenceNibble,
>> > +                u = (imm as uint<8> .>> 4) as _FenceNibble;
>> > +
>> > +            return cmd_p ? format ("fence :predecessor \"%s\" :successor 
>> > \"%s\"",
>> > +                                   u.as_string, l.as_string)
>> > +                         : format ("fence (\"%s\", \"%s\")",
>> > +                                   u.as_string, l.as_string);
>> > +          }
>> > +        assert (opcode == RV32_OPCODE_SYSTEM);
>> 
>> Ditto.
>
>
> But this `assert` is an implementation detail of `as_poke` method to make sure
> it covers all the cases and don't generate invalid strings.

Oh, ok.

>> 
>> As I see it, the to_poke methods generate Poke code that itself
>> constructs data structures... if the data provided to to_poke is invalid
>> in some way, it will be the struct constructors that should eventually
>> catch it.  Otherwise we would be replicating logic in the to_poke code.
>> And we may eventually even support non-strict construction like we do
>> with non-strict mapping.
>> 
>> Do you agree?
>> 
>
>
> Yes, a lot of my assertions are actually constraints. But there are a few
> of them that their purpose is defense programming and trying to make sure
> all pre-conditions are hold.
>
>
>> > +fun rv32_jal = (RV_Reg rd, int<32> imm) RV32_Insn:
>> > +  {
>> > +    var i = imm as RV32_Imm_J;
>> > +
>> > +    if (i.bit31)
>> > +      assert (i.bits30_21 ::: i.bit20 == 0x7ff, "invalid immediate 
>> > value");
>> > +    else
>> > +      assert (i.bits30_21 ::: i.bit20 == 0, "invalid immediate value");
>> > +    assert (i.bit0 == 0, "invalid alignment for immediate value");
>> 
>> Can these asserts be moved somehow to the constraints of either
>> RV32_Insn or RV32_InsnFmt_J?
>> 
>
>
> IMHO due to truncation rules of integers in Poke, it's a better idea to have
> these assertions here in the helper functions.
>
> Please note that this function accepts an `int<32>` immediate, but RV32I
> J-type instruction only needs `imm[20:1]` bits. So the constructor of
> `RV32_InsnFmt_J` really cannot catch our possible errors.
>
> I think, for these helper functions, it makes sense to keep the assertions.
> Otherwise, debugging could be very hard.

Ok, thanks.