Skip to content

Handle struct field write through array index in emit #72

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
angelica-moreira wants to merge 3 commits into
base: main
Choose a base branch
from
Open

Handle struct field write through array index in emit #72

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
cf75491
Emit struct field writes through array index
angelica-moreira Mar 5, 2026
47ba6f4
Add update_arr_with to Pulse.Lib.C.Array
angelica-moreira Mar 5, 2026
4f4f9f5
update the code to be more generic and emit fstar code instead of pul…
angelica-moreira Mar 5, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 9 additions & 1 deletion pulse/Pulse.Lib.C.Array.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,4 +13,12 @@ fn alloc_array u#a (#a:Type u#a) (sz:SizeT.t)

fn free_array u#a (#a:Type u#a) (r:array a)
requires A.pts_to_uninit_post r
requires freeable_array r
requires freeable_array r

fn update_arr_with (#a:Type0) (arr: array a) (idx: SizeT.t) (f: (a -> a))
requires live arr
requires with_pure (SizeT.v idx < Seq.length (value_of arr))
returns _r : unit
ensures live arr
ensures with_pure (Seq.length (value_of arr) = old (Seq.length (value_of arr)))
ensures with_pure (Seq.index (value_of arr) (SizeT.v idx) == f (old (Seq.index (value_of arr) (SizeT.v idx))))
198 changes: 134 additions & 64 deletions src/pass/emit.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -276,6 +276,7 @@ impl NameMangling {
struct Emitter<'a> {
nm: NameMangling,
diags: &'a mut Diagnostics,
in_spec: bool,
}

impl<'a> Emitter<'a> {
Expand Down Expand Up @@ -543,15 +544,36 @@ impl<'a> Emitter<'a> {
}
},
ExprT::Index(arr, idx) => {
let arr_doc = self.emit_rvalue(env, arr);
let idx_doc = self.emit_rvalue(env, idx);
ExprKind::RValue(annotated(
v,
arr_doc
.append(Doc::text(".("))
.append(idx_doc)
.append(Doc::text(")")),
))
if self.in_spec {
let arr_doc = self.emit_rvalue(env, arr);
let idx_doc = self.emit_rvalue(env, idx);
let idx_nat = match env.infer_expr(idx) {
Ok(ty) if matches!(&ty.val, TypeT::SizeT) => {
unaryfn(Doc::text("SizeT.v"), idx_doc)
}
_ => idx_doc,
};
ExprKind::RValue(annotated(
v,
parens(
Doc::text("Seq.index")
.append(Doc::line())
.append(unaryfn(Doc::text("value_of"), arr_doc))
.append(Doc::line())
.append(idx_nat),
),
))
} else {
let arr_doc = self.emit_rvalue(env, arr);
let idx_doc = self.emit_rvalue(env, idx);
ExprKind::RValue(annotated(
v,
arr_doc
.append(Doc::text(".("))
.append(idx_doc)
.append(Doc::text(")")),
))
}
}
_ => ExprKind::RValue(self.emit_rvalue_inner(env, v)),
}
Expand Down Expand Up @@ -1101,6 +1123,65 @@ impl<'a> Emitter<'a> {
})
}

fn emit_assign(&mut self, env: &Env, x: &Expr, t: &Expr) -> Doc {
if let ExprT::Member(inner, field) = &x.val {
if let ExprT::Index(arr, idx) = &inner.val {
if let Ok(elem_ty) = env.infer_expr(inner) {
let elem_ty = env.vtype_whnf(elem_ty);
if let TypeT::TypeRef(TypeRefKind::Struct(struct_name)) = &elem_ty.val {
let arr_doc = self.emit_rvalue(env, arr);
let idx_doc = self.emit_rvalue(env, idx);
let field_name = self.nm.emit(Name::StructDirectFieldName(
struct_name.val.clone(),
field.val.clone(),
));
let rhs_doc = self.emit_rvalue(env, t);
return Doc::text("let __val = ")
.append(rhs_doc)
.append(Doc::text(";"))
.append(Doc::line())
.append(Doc::text("update_arr_with"))
.append(Doc::line())
.append(arr_doc)
.append(Doc::line())
.append(idx_doc)
.append(Doc::line())
.append(Doc::text("(fun __cur -> { __cur with "))
.append(field_name)
.append(Doc::text(" = __val })"))
.append(";")
.group()
.nest(2);
}
}
}
}
if let ExprT::Index(arr, idx) = &x.val {
self.emit_rvalue(env, arr)
.append(Doc::text(".("))
.append(self.emit_rvalue(env, idx))
.append(Doc::text(")"))
.append(Doc::line())
.append("<-")
.group()
.append(Doc::line())
.append(self.emit_rvalue(env, t))
.append(";")
.group()
.nest(2)
} else {
self.emit_lvalue(env, x)
.append(Doc::line())
.append(":=")
.group()
.append(Doc::line())
.append(self.emit_rvalue(env, t))
.append(";")
.group()
.nest(2)
}
}

fn emit_stmt(&mut self, env: &Env, stmt: &Stmt) -> Doc {
annotated(stmt, {
match &stmt.val {
Expand All @@ -1114,33 +1195,7 @@ impl<'a> Emitter<'a> {
.nest(2)
.group()
}
StmtT::Assign(x, t) => {
if let ExprT::Index(arr, idx) = &x.val {
// Array write: arr.(idx) <- val;
self.emit_rvalue(env, arr)
.append(Doc::text(".("))
.append(self.emit_rvalue(env, idx))
.append(Doc::text(")"))
.append(Doc::line())
.append("<-")
.group()
.append(Doc::line())
.append(self.emit_rvalue(env, t))
.append(";")
.group()
.nest(2)
} else {
self.emit_lvalue(env, x)
.append(Doc::line())
.append(":=")
.group()
.append(Doc::line())
.append(self.emit_rvalue(env, t))
.append(";")
.group()
.nest(2)
}
}
StmtT::Assign(x, t) => self.emit_assign(env, x, t),
StmtT::If(c, b1, b2) => Doc::text("if ")
.append(parens(self.emit_rvalue(env, c)))
.nest(2)
Expand All @@ -1156,34 +1211,44 @@ impl<'a> Emitter<'a> {
requires,
ensures,
body,
} => Doc::text("while ")
.append(parens(self.emit_rvalue(env, cond)))
.append(Doc::line())
.append(Doc::concat(inv.iter().map(|inv| {
Doc::text("invariant ")
.append(self.emit_rvalue(env, inv))
.group()
.nest(2)
.append(Doc::line())
})))
.append(Doc::concat(requires.iter().map(|r| {
Doc::text("requires ")
.append(self.emit_rvalue(env, r))
.group()
.nest(2)
.append(Doc::line())
})))
.append(Doc::concat(ensures.iter().map(|e| {
Doc::text("ensures ")
.append(self.emit_rvalue(env, e))
.group()
.nest(2)
.append(Doc::line())
})))
.nest(2)
.append(self.emit_block(env, body))
.append(";")
.group(),
} => {
self.in_spec = true;
let inv_docs: Vec<_> =
inv.iter().map(|inv| self.emit_rvalue(env, inv)).collect();
let req_docs: Vec<_> =
requires.iter().map(|r| self.emit_rvalue(env, r)).collect();
let ens_docs: Vec<_> =
ensures.iter().map(|e| self.emit_rvalue(env, e)).collect();
self.in_spec = false;
Doc::text("while ")
.append(parens(self.emit_rvalue(env, cond)))
.append(Doc::line())
.append(Doc::concat(inv_docs.into_iter().map(|d| {
Doc::text("invariant ")
.append(d)
.group()
.nest(2)
.append(Doc::line())
})))
.append(Doc::concat(req_docs.into_iter().map(|d| {
Doc::text("requires ")
.append(d)
.group()
.nest(2)
.append(Doc::line())
})))
.append(Doc::concat(ens_docs.into_iter().map(|d| {
Doc::text("ensures ")
.append(d)
.group()
.nest(2)
.append(Doc::line())
})))
.nest(2)
.append(self.emit_block(env, body))
.append(";")
.group()
}
StmtT::Break => Doc::text("break;"),
StmtT::Continue => Doc::text("continue;"),
StmtT::Return(Some(t)) => Doc::text("return")
Expand Down Expand Up @@ -1712,7 +1777,9 @@ impl<'a> Emitter<'a> {
params.push(Doc::text("()"));
}

self.in_spec = true;
requires_props.extend(requires.iter().map(|r| self.emit_rvalue(env, r)));
self.in_spec = false;

let return_id = env
.push_return(ret_type.clone())
Expand All @@ -1726,7 +1793,9 @@ impl<'a> Emitter<'a> {
);
let ret_type_doc = self.emit_type(env, ret_type);

self.in_spec = true;
ensures_props.extend(ensures.iter().map(|r| self.emit_rvalue(env, r)));
self.in_spec = false;

let hdr = Doc::group(
Doc::text("fn")
Expand Down Expand Up @@ -2080,6 +2149,7 @@ pub fn emit(
let emitter = &mut Emitter {
nm: NameMangling::new(),
diags,
in_spec: false,
};
let mut output: Vec<Doc> = vec![];
output.push(Doc::text(format!(
Expand Down
33 changes: 33 additions & 0 deletions test/struct_array_write.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
#include "c2pulse.h"
#include <stddef.h>

struct point {
int x;
int y;
};

void set_x(_array struct point *pts, size_t i, int val)
_requires(i < pts._length)
_preserves_value(pts._length)
_ensures(pts[i].x == val)
{
pts[i].x = val;
}

void set_y(_array struct point *pts, size_t i, int val)
_requires(i < pts._length)
_preserves_value(pts._length)
_ensures(pts[i].y == val)
{
pts[i].y = val;
}

void set_both(_array struct point *pts, size_t i, int vx, int vy)
_requires(i < pts._length)
_preserves_value(pts._length)
_ensures(pts[i].x == vx)
_ensures(pts[i].y == vy)
{
pts[i].x = vx;
pts[i].y = vy;
}
Loading