Handle struct field write through array index in emit

[angelica-moreira]

Problem

arr[idx].field = val produces admit() in the F*/Pulse output.

In StmtT::Assign, the LHS Member(Index(arr, idx), field) falls
through to emit_lvalue. Since ExprT::Index returns ExprKind::RValue
(correct — Pulse's arr.(idx) reads without !), emit_lvalue gets an
RValue and emits TODO/admit().

Fix

Extract emit_assign() helper from emit_stmt() so the Assign arm stays inside the annotated() wrapper. Pattern-match Member(Index(arr, idx), field) in the new helper, emitting a call to update_arr_with:
pts[i].x = val;

becomes:

let __val = (!var_val); update_arr_with (!var_pts) (!var_i) (fun __cur -> { __cur with struct_point__x = __val });

update_arr_with is a new generic helper added to Pulse.Lib.C.Array.fsti that reads, applies a pure function, and writes back. Its postcondition guarantees the element at the index equals f applied to the old element, which lets F* discharge _ensures specs like pts[i].x == val.

Spec expressions (_requires, _ensures, _invariant) now emit pure F* syntax for array indexing , Seq.index (value_of arr) (SizeT.v idx) instead of the Pulse-only syntax I previous used arr.(idx).

• Scope limitation :
  • only handles one level of arr[i].field. Deeper patterns like arr[i].field.subfield or ptr->arr[i].field would need further work.

[gebner]

The early return skips the annotated wrapper, we should probably split this function in two (or make annotated take a closure).

[angelica-moreira]

ok!

[gebner]

(correct — Pulse's arr.(idx) reads without !),

Yeah, it would be a lot cleaner if we could use array_at (the indexing operation which returns a reference), but automating the separation logic conditions seems far off at this point. So we'll need special cases like this in the foreseeable future, this approach is good.

Right now the code duplicates both the arr and idx expressions, which it shouldn't (if they have side effects). We should probably generate a call to an auxiliary function like update_arr_with arr idx (fun arr_val field -> { arr_val with field }) rhs.

Please also add a test case.

[angelica-moreira]

I believe I am done. I added update_arr_with to Pulse.Lib.C.Array.fsti, I think it was that you requested, please check :). The emit_assign now emits:

let __val = (!var_val);
update_arr_with (!var_pts) (!var_i) (fun __cur -> { __cur with struct_point__x = __val });

Now we do not have more duplicated arr/idx expressions. The RHS is pre-read into a local since (!var_val) is stateful and can't go inside the lambda.

I also made spec expressions (_ensures,_requires, _invariant) emit Seq.index (value_of arr) (SizeT.v idx) instead of arr.(idx), so I believe postconditions like _ensures(pts[i].x == val) work and verify.

I added a test case like you requested, you can find it here test/struct_array_write.c with three functions (set_x, set_y, set_both), all with pre and postconditions.

[gebner]

I believe I am done. I added update_arr_with to Pulse.Lib.C.Array.fsti, I think it was that you requested, please check :). The emit_assign now emits:

let __val = (!var_val); update_arr_with (!var_pts) (!var_i) (fun __cur -> { __cur with struct_point__x = __val });

Can you please turn this into:

update_arr_with (!var_pts) (!var_i) (fun __cur __val -> { __cur with struct_point__x = __val }) (!var_val)

I'd really like to avoid generating extra let-bindings here (which might break when we start supporting things like a[i].x = a[j].x = 67).

I also made spec expressions (_ensures,_requires, _invariant) emit Seq.index (value_of arr) (SizeT.v idx) instead of arr.(idx), so I believe postconditions like _ensures(pts[i].x == val) work and verify.

There is no need to do that distinction, and I'd really like to avoid it (to avoid potential divergence in behavior).

I tried removing the is_spec handling, and what breaks is that we were missing parentheses around the Pulse term for ExprT::Index. Please just add the parentheses instead.

I added a test case like you requested, you can find it here test/struct_array_write.c with three functions (set_x, set_y, set_both), all with pre and postconditions.

The test case is great, thanks.