Fix Python->Laurel: Havoc callee or Heap after unmodeled InstanceCall

[thanhnguyen-aws]

Fixes: #977

Problem

When the Python→Laurel translator encounters an unmodeled instance call (e.g., xs.some_method()), it previously only havocked maybe_except. It did not account for the fact that the unmodeled call could mutate the receiver or heap-allocated fields, leading to unsound verification results where the verifier assumed variables retained their pre-call values.

For example, after xs.some_unmodeled_call(), the verifier would still prove xs == [1, 2] — incorrectly, since the call could have mutated xs.

Fix

Introduces mkHavocStmtsForUnmodeledCall, a centralized helper that computes the correct set of havoc statements for any unmodeled call. The helper is used in both translateAssign (for y = x.method()) and translateStmt (for bare x.method() calls), replacing the previous inline holeExceptHavoc logic.

For an unmodeled call, the helper emits:

1. Always: havoc maybe_except (the call could throw)
2. If the receiver is a non-composite variable (e.g., a list): havoc the receiver variable (the method could mutate it)
3. If the receiver is composite, or any argument is composite: havoc $heap (the method could mutate heap-allocated fields)

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[shigoel]

@thanhnguyen-aws Can you please add some tests here?

[thanhnguyen-aws]

@thanhnguyen-aws Can you please add some tests here?

I added an expected test.

[shigoel]

Review Summary

The fix is logically sound — when an unmodeled instance method call (e.g., xs.some_unmodeled_call(3)) is a black box, the receiver should be havocked since the method could mutate it. The implementation is correct for the standalone expression case.

Soundness gap in translateAssign

The PR only adds callee havocking in the .Expr _ value case (standalone expression statements). But y = xs.some_unmodeled_call(3) goes through translateAssign where the RHS is an unmodeled Call → Hole. The Hole case (lines 1132–1160) havocs maybe_except but does not havoc the callee. This is the same soundness gap the PR intends to fix — it's just not covered in the assignment case.

Test coverage

Only one test for the happy path. Consider adding:

• y = xs.method() (assignment form — exercises the translateAssign path)
• a.b.method() (chained attribute — verifies correct base extraction)
• Non-variable base like get_list().method() (should NOT havoc)

No performance concerns — the membership check pattern matches the rest of the file.

[MikaelMayer]

I haven't read the PR but it seems that if a method name is not recognized, we should just havoc the heap and that's it. The receiver is just a special case.

[shigoel]

@thanhnguyen-aws Could you please address @MikaelMayer's comment re. the design here?

[thanhnguyen-aws]

I haven't read the PR but it seems that if a method name is not recognized, we should just havoc the heap and that's it. The receiver is just a special case.

I added Heap havocking for cases when inputs of the unmodeled function call contains Class type. Note that List and Dict are currently wrapped by Any type and separated from the Heap, so we need to havoc them separately.

[MikaelMayer]

Super nice tests. You might consider updating the PR description and title.

[shigoel]

Review from Claude Code — 1 soundness concern, 1 invariant suggestion, 1 minor style nit.

[shigoel]

LGTM — soundness gap for composite receivers is fixed, invariant is documented, tests cover the key cases. Two minor style nits (missing space in let inputExprs:=, Prod.fst vs destructuring) but nothing blocking.

[shigoel]

@thanhnguyen-aws Please update the PR description.

[keyboardDrummer]

I think the right design here needs a Laurel change. When calling an unmodeled thing, we should call a Laurel procedure like this:

procedure Unmodelled() returns (maybe_except: ...)
  modifies *
  opaque;

The modifies * is currently missing in Laurel, which is why this PR had to refer to $heap. The follwoing in progress PR keyboardDrummer#12 adds wildcard * to Laurel, but we can also create a separate PR for adding modifies * to Laurel, which might be the fastest way forward.

[keyboardDrummer]

Asked a bot to create a separate PR for adding modifies *: #1030