parsing of record field names that collide with variable names

[Smattr]

Hello there,

I am implementing an automated translator to Uclid5 from another verification language. One of the automated translations produced an unexpected outcome and I ~minimized it to the following:

module main {
  type t = record {
    x : integer
  };
  var x : t;

  procedure foo()
    modifies x;
  {
    if (x.x == x.x) {
    }
  }
}

Uclid5 0.9.5 has the following to say about this input:

$ uclid foo.ucl
Type error at line 10: Argument to select operator must be of type record or instance.
    if (x.x == x.x) {
        ^
Type error at line 10: Argument to select operator must be of type record or instance.
    if (x.x == x.x) {
               ^
Parsing failed. 2 errors found.

Is this expected? In my thinking, x is a record instance. But Uclid5 does not seem to enjoy its field having the same name.

A related (?) issue I ran into is doing assignment to a field within an array of records. This is actually done within the test/record-array.ucl file in the Uclid5 repository:

arr[0].a = 10;

However, this looks invalid according to the grammar in the tutorial, and is rejected:

$ uclid test/record-array.ucl
Syntax error test/record-array.ucl, line 10: '`='' expected but `.' found.
    arr[0].a = 10;
          ^

If there's a work around for this, I'd be interested to know, as I'm currently not sure how I'll translate expressions like this.

[polgreen]

Hi Matt,

Is this expected? In my thinking, x is a record instance. But Uclid5 does not seem to enjoy its field having the same name.

Let's say I don't think this is deliberate but I am not surprised.. can you work around by having different names and I'll look into it. At the very least we should throw a more meaningful error.

arr[0].a = 10;

Yes, we currently don't parse this, it's on my list of things to add. It's a bit laborious, especially with a big record type, but instead you can write:

arr[0] = {10, arr[0].b};

Thanks for the minimal bug reports!

[Smattr]

Hi Elizabeth, thanks for the speedy reply!

Renaming the field might be a little complicated, as I'm translating user input so they're free to write whatever's legal in the source language (Murphi). I might have to just detect and reject input like this.

Thanks for the record work around. I think this is achievable, but I have to think more deeply about it. Murphi unfortunately allows arbitrary nesting here so a naive translation might produce things like a[0].b.c[2].d[3].

[polgreen]

Ok, I'll aim to have a look at both the issues next week and let you know

[Smattr]

I realized the work around for array assignment actually won't work for my use case. Coming from Murphi, the index can be a variable. E.g. the originating Murphi code might look like:

procedure foo(var r: complex_type_t; var i: 0..10); begin
  r[i].a := 10;
end;

I can't think of a way to translate this to Uclid5 other than some kind of 11-alternative if-then-else branch on the value of i. Obviously this also causes complications if i is not just a variable but a more complex expression like a call to an impure function. E.g. r[my_func()].a := 10.

Because this is all related to generated code from artificial test cases, I think you should probably ignore this issue for now. Maybe something to revisit if another user has a real world model that hits this problem.