fix(laurel): local variable no longer shadows output parameter

[fabiomadge]

Fixes #567.

Problem

When a Laurel procedure declares a local variable with the same name as an output parameter (e.g. var result: int := x + x in a procedure with returns (result: int)), the generated Core emits init result inside the $body block, which shadows the output parameter. The return statement then assigns the local to itself, and the output parameter is never written.

Fix

In translateStmt for LocalVariable: when the variable name matches an output parameter, emit set/havoc instead of init, since the variable already exists in Core as the output parameter.

• init name type (some expr) → set name expr
• init name type none → havoc name
• init before call → dropped (the call writes to the existing variable directly)

Before

procedure double (x : int) returns (result : int)
{
  $body: {
    var result : int := x + x;   // shadows output param
    result := result;            // self-assignment on local
    exit $body;
  }
};

After

procedure double (x : int) returns (result : int)
{
  $body: {
    result := x + x;             // assigns to output param
    result := result;            // harmless self-assignment
    exit $body;
  }
};

Tests

New test T18_LocalVarShadowsOutput covers five cases:

1. Expression initializer with auto-generated result name
2. Expression initializer with user-named output param
3. No initializer (havoc path)
4. Procedure call as initializer
5. Output param used as scratch, then overwritten by return

[keyboardDrummer]

This PR changes Laurel in a way that I think is confusing.

What happens if I do:

procedure double(x: int) returns (result: int)
  ensures result == 1
{
  result := 1;
  var result: int := 23;
  return;
};

Would that fail?

Instead of what this PR does, I'd rather add a feature to Laurel that enables anonymous return variables, so we can replace the code that creates a "result" return variable.

We could also consider adding an option that disallows shadowing of return parameters.

[fabiomadge]

Verification fails for the example you provided, as result becomes 23. I don't think there is any situation where a Laurel user should see Core type-checking errors. I don't understand what value anonymous return values add to a language not primarily targeted at humans, to make them worth the added complexity. I'm fine with preventing users from redeclaring return values, but that seems like a different PR to me. We should close this PR if you object to the change.

[keyboardDrummer]

Verification fails for the example you provided, as result becomes 23.

That seems wrong

I don't think there is any situation where a Laurel user should see Core type-checking errors.

Agreed. Laurel's resolution phase should prevent that.

I don't understand what value anonymous return values add to a language not primarily targeted at humans, to make them worth the added complexity.

Because then the languages building on top of Laurel don't have to come up with names for the output parameters when there is no name in the user program, which gives them the problem of having to come up with a unique name, a problem that Laurel can solve for them.