extra fallback case statement in Sail model that isn't there in ASL

[cfbolz]

Maybe this should be an issue in the asl_to_sail repo, but I discovered the following today:

The following asl function:

// TGxGranuleBits()
// ================
// Retrieve the address size, in bits, of a granule

integer TGxGranuleBits(TGx tgx)
    case tgx of
        when TGx_4KB  return 12;
        when TGx_16KB return 14;
        when TGx_64KB return 16;

gets translated into the following Sail function:

function TGxGranuleBits tgx = {
    match tgx {
      TGx_4KB => {
          return(12)
      },
      TGx_16KB => {
          return(14)
      },
      TGx_64KB => {
          return(16)
      },
      _ => {
          return(undefined : int)
      }
    }
}

Why does the extra fallback case returning an undefined int get added? The match in the asl code is exhaustive and indeed Sail then complains about it:

Warning: Redundant case src/v8_base.sail:9070.6-7:            ] 7% (1768/24545)          
9070 |      _ => {
     |      ^
     | 
This match case is never used

However, despite the Sail compiler complaining about the case being redundant, the fallback case still exists in the C code. I suspect this is what causes the result of TGxGranuleBits to be a sail_int and the arithmetic that is then performed on the result is also operating on sail_int, not mach_int.

This came up because I am looking into integers that Sail can't prove to fit into machine words in the ARM model, because those are one of the main sources of emulator slowness in my pydrofoil-arm emulator. I can partly fix this on the Pydrofoil side, but maybe it would make sense to fix this more generally? /cc @martinberger

[bauereiss]

Thanks for the report. There indeed seem to be some bugs in asl_to_sail around incomplete pattern matches. I think I know how to fix the one that leads to the particular redundant fall-through case above, although there seem to be some more cases that I'm currently investigating. I've opened pull request #17 with a preliminary update to sail-arm. This also changes the behaviour of the fall-through cases to raise an error rather than allowing undefined behaviour, which seems like a dubious decision in hindsight. Raising an error should better reflect the intended ASL semantics.

Having said all that, it's not entirely clear to me whether this will fix your original performance problem. When I generate a C emulator from the updated Sail, the above function still has a sail_int return type. Maybe there's further work to be done in Sail itself.

[cfbolz]

@bauereiss this is very cool, thank you! is there a chance you could do the same thing for the v9.3 model too? I didn't switch to the 9.4 one yet.

Also, out of interest, could you point me to the corresponding asl_to_sail changes? or are those not public?

[bauereiss]

Sorry for the delay, I got distracted. Is there something holding you back from switching to v9.4, or have you just not gotten around to it? I'm asking because regenerating the v9.3 model now would require some work on updating the manual patches that we use in the translation process, due to a number of changes in Sail and asl_to_sail since we originally generated that model. I'd have to see if I can find time to do that, if you need it.

The asl_to_sail patch I've used before the holidays was still a work-in-progress, but I've pushed it to a branch for now. I should make it less hacky at some point.

[cfbolz]

@bauereiss Sorry, yes, I should just switch to v9.4 (it involves also updating my pinned sail and isla repos, which is always a little bit annoying). I've started working on it now, will let you know if I hit any problems.

[cfbolz]

ok, I can confirm that both the v9.4 version on HEAD as well as on your PR work for me. There is unfortunately not really a measurable performance difference, even though the generated code from your PR looks clearly "better". v9.4 is a bit slower than v9.3 on pydrofoil, for me (about 25%), but that's probably fixable and not entirely surprising, given some of the new features (eg the PMU adds a bit of overhead to every instruction, even it it's turned off). Sidenote: the Sail C emulator got a lot faster from 9.3 to 9.4 (maybe 4x?), but I haven't looked properly why.

From my POV it would still be very cool to merge this!