Skip to content

Commit 2bcc553

Browse files
gebnerCopilot
andcommitted
Fix const detection and add #p to struct assume vals
- Detect const on any parameter type (not just pointers), supporting const structs with nested pointers - Add (#p: perm) to struct unfold/fold/getter assume vals - Keep pointee-const detection for const int *x pattern Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
1 parent 3191d80 commit 2bcc553

2 files changed

Lines changed: 17 additions & 5 deletions

File tree

cpp/impl.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -794,6 +794,8 @@ class C2PulseConsumer : public ASTConsumer {
794794
? ir::ParamMode::Consumed()
795795
: [&]() {
796796
auto qt = param->getType().IgnoreParens();
797+
if (qt.isConstQualified())
798+
return ir::ParamMode::Const();
797799
if (auto ptr = dyn_cast<PointerType>(qt)) {
798800
if (ptr->getPointeeType().isConstQualified())
799801
return ir::ParamMode::Const();

src/pass/emit.rs

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1638,6 +1638,7 @@ impl<'a> Emitter<'a> {
16381638
.append(Doc::line())
16391639
.append(ref_struct_type.clone()),
16401640
),
1641+
parens(Doc::text("#p: perm")),
16411642
parens(
16421643
Doc::text("vx:")
16431644
.append(Doc::line())
@@ -1652,6 +1653,7 @@ impl<'a> Emitter<'a> {
16521653
naryfn([
16531654
Doc::text("Pulse.Lib.Reference.pts_to"),
16541655
Doc::text("x"),
1656+
Doc::text("#p"),
16551657
Doc::text("vx"),
16561658
]),
16571659
{
@@ -1660,6 +1662,7 @@ impl<'a> Emitter<'a> {
16601662
post.push(naryfn([
16611663
Doc::text("Pulse.Lib.Reference.pts_to"),
16621664
unaryfn(self.nm.emit(ghost_fld(fld)), Doc::text("x")),
1665+
Doc::text("#p"),
16631666
Doc::text("vx.").append(self.nm.emit(direct_fld(fld))),
16641667
]));
16651668
}
@@ -1677,11 +1680,14 @@ impl<'a> Emitter<'a> {
16771680
self.nm
16781681
.emit(Name::StructAuxFn(name.val.clone(), "raw_fold".into())),
16791682
&{
1680-
let mut args = vec![parens(
1681-
Doc::text("x:")
1682-
.append(Doc::line())
1683-
.append(ref_struct_type.clone()),
1684-
)];
1683+
let mut args = vec![
1684+
parens(
1685+
Doc::text("x:")
1686+
.append(Doc::line())
1687+
.append(ref_struct_type.clone()),
1688+
),
1689+
parens(Doc::text("#p: perm")),
1690+
];
16851691
for (fld, _) in fields {
16861692
args.push(fold_arg_name(fld))
16871693
}
@@ -1697,6 +1703,7 @@ impl<'a> Emitter<'a> {
16971703
pre.push(naryfn([
16981704
Doc::text("Pulse.Lib.Reference.pts_to"),
16991705
unaryfn(self.nm.emit(ghost_fld(fld)), Doc::text("x")),
1706+
Doc::text("#p"),
17001707
fold_arg_name(fld),
17011708
]));
17021709
}
@@ -1705,6 +1712,7 @@ impl<'a> Emitter<'a> {
17051712
mk_thunk(naryfn([
17061713
Doc::text("Pulse.Lib.Reference.pts_to"),
17071714
Doc::text("x"),
1715+
Doc::text("#p"),
17081716
Doc::text("{")
17091717
.append(Doc::concat(fields.iter().map(|(fld, _)| {
17101718
Doc::line()
@@ -1761,6 +1769,7 @@ impl<'a> Emitter<'a> {
17611769
let fld_pts_to = naryfn([
17621770
Doc::text("pts_to"),
17631771
unaryfn(self.nm.emit(ghost_fld(fld)), Doc::text("x")),
1772+
Doc::text("#p"),
17641773
Doc::text("vx"),
17651774
]);
17661775
ses.push(mk_assume_val(
@@ -1772,6 +1781,7 @@ impl<'a> Emitter<'a> {
17721781
.append(Doc::line())
17731782
.append(ref_struct_type.clone()),
17741783
),
1784+
parens(Doc::text("#p: perm")),
17751785
parens(
17761786
Doc::text("#vx:")
17771787
.append(Doc::line())

0 commit comments

Comments
 (0)