Give each declined optional parameter its own null - #243
Draft
nikswamy wants to merge 2 commits into
Draft
Conversation
A call that declines several `_nullable` outputs passes the same `NULL`
for each and gets back one `unless_null null _` per declined output.
Those guards are identical apart from the resource they carry, and the
resource is exactly the implicit `elim_null_ref` has to recover by
matching. With more than one in scope the match is ambiguous, the prover
falls back to the introduction rules, and the whole thing surfaces as
Could not solve typeclass constraint 'has_is_null (*?u3813*)_'
pointed at the entire body, naming a typeclass that appears nowhere in
the C and nowhere in the annotations.
Two plausible-looking fixes do not work. Writing the pointee type down
does not help, because the pointee was never the ambiguous implicit.
Nor does bundling the eliminations into one lemma that takes both
guards: the matcher solves the conjuncts one at a time and the first is
still ambiguous.
Split the guards apart at the pointer instead of at the resource.
`Pulse.Lib.C.Nullable.null_ref` returns a null pointer bound to a name
and says in its post-condition that it is null; emit one per declined
output and pass the names. The guards then differ in a position the
matcher can discriminate on, and the eliminations go through unchanged.
Nothing is hidden from the caller -- the value is still null and the
post-condition says so -- only from the term matcher, which is the
point.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d
(cherry picked from commit eca2b11)
An optional const parameter states its guarded resource with the permission and the pointee value the caller handed in, both implicits of the signature, so that `preserves` can give the caller back the very hold it passed rather than a fresh one. A call site that declines the parameter holds nothing to solve those implicits against, and the application does not elaborate: the failure surfaces as unresolved unification variables in the term, naming neither the parameter nor the implicit it is about. Because the pointer is null the guard is `emp`, so any resource at all may be introduced under it. Write one down at the call site with no metavariables left in it -- full permission and the pointee type's canonical zero -- and both implicits are pinned by structural match. It asserts nothing about memory, there being no memory to assert anything about. Only a const parameter needs this. Every other mode already binds its guarded value existentially, which a null call site discharges with no witness at all; writing the guard down there would instead ask the prover for a `pts_to` on the pointee that it does not have. Callers previously had to work around this by declaring such parameters mutable, which forces full permission on the parameter and so locks out any caller that holds only a fraction of the argument. The new test covers all three sides: declining the input, forwarding it, and supplying a member of a structure the caller itself only borrows. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit f58d84b)
Contributor
|
!diff |
Generated F* output diffEffect of this pull request on the F* code SummaryFull diff: full diff artifact Diffdiff --git base/const_typedef/Func_call_read_optional.fst head/const_typedef/Func_call_read_optional.fst
index a5a518e..018cb0c 100644
--- base/const_typedef/Func_call_read_optional.fst
+++ head/const_typedef/Func_call_read_optional.fst
@@ -11,6 +11,7 @@ divergent fn func_call_read_optional ()
Pulse.Lib.Reference.pts_to_not_null (var_x);
(Func_read_optional.func_read_optional var_x);
Pulse.Lib.C.Nullable.elim_unless_null_ref (var_x);
- (Func_read_optional.func_read_optional null);
- Pulse.Lib.C.Nullable.elim_null_ref null;
+ let __pal_null_1 = Pulse.Lib.C.Nullable.null_ref (Int32.t);
+ (Func_read_optional.func_read_optional __pal_null_1);
+ Pulse.Lib.C.Nullable.elim_null_ref __pal_null_1;
}
\ No newline at end of file
diff --git head/nullable_const_in/Func_call_borrowed_member.fst head/nullable_const_in/Func_call_borrowed_member.fst
new file mode 100644
index 0000000..625717d
--- /dev/null
+++ head/nullable_const_in/Func_call_borrowed_member.fst
@@ -0,0 +1,17 @@
+module Func_call_borrowed_member
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_call_borrowed_member (var_q: Typedef_PCPair.ty_pcpair)
+ preserves (Typedef_PCPair.ty_pcpair__pred var_q 'p_q_0 'val_q_0)
+ returns return_1 : Typedef_uint32_t.ty_uint32_t
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
+{
+ let mut var_q = var_q;
+ let mut var_result : Typedef_uint32_t.ty_uint32_t;
+ Pulse.Lib.Reference.pts_to_not_null ((Struct_Pair.struct_pair__get_a (!var_q)));
+ var_result := (Func_read_optional.func_read_optional (Struct_Pair.struct_pair__get_a (!var_q)));
+ Pulse.Lib.C.Nullable.elim_unless_null_ref ((Struct_Pair.struct_pair__get_a (!var_q)));
+ return (!var_result);
+}
\ No newline at end of file
diff --git head/nullable_const_in/Func_call_borrowed_member.fsti head/nullable_const_in/Func_call_borrowed_member.fsti
new file mode 100644
index 0000000..e6c8492
--- /dev/null
+++ head/nullable_const_in/Func_call_borrowed_member.fsti
@@ -0,0 +1,9 @@
+module Func_call_borrowed_member
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_call_borrowed_member (var_q: Typedef_PCPair.ty_pcpair)
+preserves (Typedef_PCPair.ty_pcpair__pred var_q 'p_q_0 'val_q_0)
+returns return_1 : Typedef_uint32_t.ty_uint32_t
+ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
\ No newline at end of file
diff --git head/nullable_const_in/Func_call_declined.fst head/nullable_const_in/Func_call_declined.fst
new file mode 100644
index 0000000..a148099
--- /dev/null
+++ head/nullable_const_in/Func_call_declined.fst
@@ -0,0 +1,19 @@
+module Func_call_declined
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_call_declined ()
+ returns return_1 : Typedef_uint32_t.ty_uint32_t
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
+{
+ let mut var_result : Typedef_uint32_t.ty_uint32_t;
+ let __pal_null_1 = Pulse.Lib.C.Nullable.null_ref (Typedef_Point.ty_point);
+ Pulse.Lib.C.Nullable.intro_unless_null_null_ref __pal_null_1 (((Typedef_PCPoint.ty_pcpoint__pred
+ __pal_null_1
+ 1.0R
+ zero_default)));
+ var_result := (Func_read_optional.func_read_optional __pal_null_1);
+ Pulse.Lib.C.Nullable.elim_null_ref __pal_null_1;
+ return (!var_result);
+}
\ No newline at end of file
diff --git head/nullable_const_in/Func_call_declined.fsti head/nullable_const_in/Func_call_declined.fsti
new file mode 100644
index 0000000..edeb75b
--- /dev/null
+++ head/nullable_const_in/Func_call_declined.fsti
@@ -0,0 +1,8 @@
+module Func_call_declined
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_call_declined ()
+returns return_1 : Typedef_uint32_t.ty_uint32_t
+ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
\ No newline at end of file
diff --git head/nullable_const_in/Func_call_forwarded.fst head/nullable_const_in/Func_call_forwarded.fst
new file mode 100644
index 0000000..2ba1ad3
--- /dev/null
+++ head/nullable_const_in/Func_call_forwarded.fst
@@ -0,0 +1,15 @@
+module Func_call_forwarded
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_call_forwarded (var_p: Typedef_PCPoint.ty_pcpoint)
+ preserves (unless_null var_p (((Typedef_PCPoint.ty_pcpoint__pred var_p 'p_p_0 'val_p_0))))
+ returns return_1 : Typedef_uint32_t.ty_uint32_t
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
+{
+ let mut var_p = var_p;
+ let mut var_result : Typedef_uint32_t.ty_uint32_t;
+ var_result := (Func_read_optional.func_read_optional (!var_p));
+ return (!var_result);
+}
\ No newline at end of file
diff --git head/nullable_const_in/Func_call_forwarded.fsti head/nullable_const_in/Func_call_forwarded.fsti
new file mode 100644
index 0000000..7b633f6
--- /dev/null
+++ head/nullable_const_in/Func_call_forwarded.fsti
@@ -0,0 +1,9 @@
+module Func_call_forwarded
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_call_forwarded (var_p: Typedef_PCPoint.ty_pcpoint)
+preserves (unless_null var_p (((Typedef_PCPoint.ty_pcpoint__pred var_p 'p_p_0 'val_p_0))))
+returns return_1 : Typedef_uint32_t.ty_uint32_t
+ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
\ No newline at end of file
diff --git head/nullable_const_in/Func_read_optional.fst head/nullable_const_in/Func_read_optional.fst
new file mode 100644
index 0000000..95a219e
--- /dev/null
+++ head/nullable_const_in/Func_read_optional.fst
@@ -0,0 +1,31 @@
+module Func_read_optional
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_read_optional (var_p: Typedef_PCPoint.ty_pcpoint)
+ preserves (unless_null var_p (((Typedef_PCPoint.ty_pcpoint__pred var_p 'p_p_0 'val_p_0))))
+ returns return_1 : Typedef_uint32_t.ty_uint32_t
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
+{
+ let mut var_p = var_p;
+ let mut var_result : Typedef_uint32_t.ty_uint32_t;
+ if ((not (Pulse.Lib.Reference.is_null (!var_p)))) {
+ let var___pal_guarded_0 = ((!var_p));
+ Pulse.Lib.C.Nullable.elim_unless_null_ref var___pal_guarded_0;
+ var_result := (!(Struct_Point.struct_point__get_x (!var_p)));
+ assert (Pulse.Lib.C.Nullable.unless_null var___pal_guarded_0 (((Typedef_PCPoint.ty_pcpoint__pred
+ var___pal_guarded_0
+ 'p_p_0
+ 'val_p_0))));
+ } else {
+ let var___pal_guarded_0 = ((!var_p));
+ Pulse.Lib.C.Nullable.elim_null_ref var___pal_guarded_0;
+ var_result := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ assert (Pulse.Lib.C.Nullable.unless_null var___pal_guarded_0 (((Typedef_PCPoint.ty_pcpoint__pred
+ var___pal_guarded_0
+ 'p_p_0
+ 'val_p_0))));
+ };
+ return (!var_result);
+}
\ No newline at end of file
diff --git head/nullable_const_in/Func_read_optional.fsti head/nullable_const_in/Func_read_optional.fsti
new file mode 100644
index 0000000..3ac5a96
--- /dev/null
+++ head/nullable_const_in/Func_read_optional.fsti
@@ -0,0 +1,9 @@
+module Func_read_optional
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_read_optional (var_p: Typedef_PCPoint.ty_pcpoint)
+preserves (unless_null var_p (((Typedef_PCPoint.ty_pcpoint__pred var_p 'p_p_0 'val_p_0))))
+returns return_1 : Typedef_uint32_t.ty_uint32_t
+ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
\ No newline at end of file
diff --git head/nullable_const_in/Struct_Pair.fst head/nullable_const_in/Struct_Pair.fst
new file mode 100644
index 0000000..fc3708d
--- /dev/null
+++ head/nullable_const_in/Struct_Pair.fst
@@ -0,0 +1,99 @@
+module Struct_Pair
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+noeq type struct_pair = {
+ struct_pair__a: Typedef_Point.ty_point;
+ struct_pair__b: Typedef_Point.ty_point;
+}
+assume val struct_pair__sizeof_pos (a: Type0 { a == struct_pair }) :
+ Lemma
+ ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
+ [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+[@@pulse_eager_unfold] let predicate struct_pair__pred ([@@@mkey] this: struct_pair) (p: perm) =
+ ((Typedef_Point.ty_point__pred this.struct_pair__a p) **
+ (Typedef_Point.ty_point__pred this.struct_pair__b p))
+[@@pulse_eager_unfold] let predicate struct_pair__uninit_pred ([@@@mkey] this: struct_pair) =
+ ((Typedef_Point.ty_point__uninit_pred this.struct_pair__a) **
+ (Typedef_Point.ty_point__uninit_pred this.struct_pair__b))
+assume val struct_pair__aux_raw_unfolded ([@@@mkey] x: (ref struct_pair)) (p: perm) : slprop
+assume val struct_pair__a_1 (x: (ref struct_pair)) : GTot (ref Typedef_Point.ty_point)
+assume val struct_pair__b_1 (x: (ref struct_pair)) : GTot (ref Typedef_Point.ty_point)
+assume val struct_pair__a_container (r: (ref Typedef_Point.ty_point)) : (ref struct_pair)
+assume val struct_pair__a_container_inv (p: (ref struct_pair)) :
+ Lemma
+ (ensures (struct_pair__a_container (struct_pair__a_1 p)) == p)
+ [SMTPat (struct_pair__a_container (struct_pair__a_1 p))]
+assume val struct_pair__a_proj_container_inv (r: (ref Typedef_Point.ty_point)) :
+ Lemma
+ (ensures (struct_pair__a_1 (struct_pair__a_container r)) == r)
+ [SMTPat (struct_pair__a_1 (struct_pair__a_container r))]
+assume val struct_pair__b_container (r: (ref Typedef_Point.ty_point)) : (ref struct_pair)
+assume val struct_pair__b_container_inv (p: (ref struct_pair)) :
+ Lemma
+ (ensures (struct_pair__b_container (struct_pair__b_1 p)) == p)
+ [SMTPat (struct_pair__b_container (struct_pair__b_1 p))]
+assume val struct_pair__b_proj_container_inv (r: (ref Typedef_Point.ty_point)) :
+ Lemma
+ (ensures (struct_pair__b_1 (struct_pair__b_container r)) == r)
+ [SMTPat (struct_pair__b_1 (struct_pair__b_container r))]
+assume val struct_pair__a_proj_null :
+ (squash
+ ((struct_pair__a_1 (Pulse.Lib.Reference.null #(struct_pair))) ==
+ (Pulse.Lib.Reference.null #(Typedef_Point.ty_point))))
+[@@pulse_intro]
+assume val struct_pair__aux_raw_unfold (x: (ref struct_pair)) (#p: perm) (vx: struct_pair) :
+ (stt_ghost
+ unit
+ emp_inames
+ (Pulse.Lib.Reference.pts_to x #p vx)
+ (fun _ ->
+ ((struct_pair__aux_raw_unfolded x p) **
+ (Pulse.Lib.Reference.pts_to (struct_pair__a_1 x) #p vx.struct_pair__a) **
+ (Pulse.Lib.Reference.pts_to (struct_pair__b_1 x) #p vx.struct_pair__b))))
+[@@pulse_intro]
+assume val struct_pair__aux_raw_fold (x: (ref struct_pair)) (#p: perm) v_a v_b :
+ (stt_ghost
+ unit
+ emp_inames
+ ((struct_pair__aux_raw_unfolded x p) **
+ (Pulse.Lib.Reference.pts_to (struct_pair__a_1 x) #p v_a) **
+ (Pulse.Lib.Reference.pts_to (struct_pair__b_1 x) #p v_b))
+ (fun _ -> (Pulse.Lib.Reference.pts_to x #p { struct_pair__a=v_a; struct_pair__b=v_b; })))
+[@@pulse_intro]
+assume val struct_pair__aux_raw_fold_uninit (x: (ref struct_pair)) :
+ (stt_ghost
+ unit
+ emp_inames
+ ((struct_pair__aux_raw_unfolded x 1.0R) **
+ (Pulse.Lib.Reference.pts_to_uninit (struct_pair__a_1 x)) **
+ (Pulse.Lib.Reference.pts_to_uninit (struct_pair__b_1 x)))
+ (fun _ -> (Pulse.Lib.Reference.pts_to_uninit x)))
+assume val struct_pair__aux_raw_unfold_uninit (x: (ref struct_pair)) :
+ (stt_ghost
+ unit
+ emp_inames
+ (Pulse.Lib.Reference.pts_to_uninit x)
+ (fun _ ->
+ ((struct_pair__aux_raw_unfolded x 1.0R) **
+ (Pulse.Lib.Reference.pts_to_uninit (struct_pair__a_1 x)) **
+ (Pulse.Lib.Reference.pts_to_uninit (struct_pair__b_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_pair__get_a (x: (ref struct_pair)) (#p: perm) :
+ (stt_atomic
+ (ref Typedef_Point.ty_point)
+ #PulseCore.Observability.Neutral
+ emp_inames
+ (struct_pair__aux_raw_unfolded x p)
+ (fun vx' -> ((struct_pair__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_pair__a_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_pair__get_b (x: (ref struct_pair)) (#p: perm) :
+ (stt_atomic
+ (ref Typedef_Point.ty_point)
+ #PulseCore.Observability.Neutral
+ emp_inames
+ (struct_pair__aux_raw_unfolded x p)
+ (fun vx' -> ((struct_pair__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_pair__b_1 x)))))
+instance has_zero_default_struct_pair : (has_zero_default struct_pair) =
+ { zero_default = { struct_pair__a = zero_default; struct_pair__b = zero_default; } }
\ No newline at end of file
diff --git head/nullable_const_in/Struct_Point.fst head/nullable_const_in/Struct_Point.fst
new file mode 100644
index 0000000..8f2a00f
--- /dev/null
+++ head/nullable_const_in/Struct_Point.fst
@@ -0,0 +1,101 @@
+module Struct_Point
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+noeq type struct_point = {
+ struct_point__x: Typedef_uint32_t.ty_uint32_t;
+ struct_point__y: Typedef_uint32_t.ty_uint32_t;
+}
+assume val struct_point__sizeof_pos (a: Type0 { a == struct_point }) :
+ Lemma
+ ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
+ [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+[@@pulse_eager_unfold] let predicate struct_point__pred ([@@@mkey] this: struct_point) (p: perm) =
+ ((Typedef_uint32_t.ty_uint32_t__pred this.struct_point__x p) **
+ (Typedef_uint32_t.ty_uint32_t__pred this.struct_point__y p))
+[@@pulse_eager_unfold] let predicate struct_point__uninit_pred ([@@@mkey] this: struct_point) =
+ ((Typedef_uint32_t.ty_uint32_t__uninit_pred this.struct_point__x) **
+ (Typedef_uint32_t.ty_uint32_t__uninit_pred this.struct_point__y))
+assume val struct_point__aux_raw_unfolded ([@@@mkey] x: (ref struct_point)) (p: perm) : slprop
+assume val struct_point__x_1 (x: (ref struct_point)) : GTot (ref Typedef_uint32_t.ty_uint32_t)
+assume val struct_point__y_1 (x: (ref struct_point)) : GTot (ref Typedef_uint32_t.ty_uint32_t)
+assume val struct_point__x_container (r: (ref Typedef_uint32_t.ty_uint32_t)) : (ref struct_point)
+assume val struct_point__x_container_inv (p: (ref struct_point)) :
+ Lemma
+ (ensures (struct_point__x_container (struct_point__x_1 p)) == p)
+ [SMTPat (struct_point__x_container (struct_point__x_1 p))]
+assume val struct_point__x_proj_container_inv (r: (ref Typedef_uint32_t.ty_uint32_t)) :
+ Lemma
+ (ensures (struct_point__x_1 (struct_point__x_container r)) == r)
+ [SMTPat (struct_point__x_1 (struct_point__x_container r))]
+assume val struct_point__y_container (r: (ref Typedef_uint32_t.ty_uint32_t)) : (ref struct_point)
+assume val struct_point__y_container_inv (p: (ref struct_point)) :
+ Lemma
+ (ensures (struct_point__y_container (struct_point__y_1 p)) == p)
+ [SMTPat (struct_point__y_container (struct_point__y_1 p))]
+assume val struct_point__y_proj_container_inv (r: (ref Typedef_uint32_t.ty_uint32_t)) :
+ Lemma
+ (ensures (struct_point__y_1 (struct_point__y_container r)) == r)
+ [SMTPat (struct_point__y_1 (struct_point__y_container r))]
+assume val struct_point__x_proj_null :
+ (squash
+ ((struct_point__x_1 (Pulse.Lib.Reference.null #(struct_point))) ==
+ (Pulse.Lib.Reference.null #(Typedef_uint32_t.ty_uint32_t))))
+[@@pulse_intro]
+assume val struct_point__aux_raw_unfold (x: (ref struct_point)) (#p: perm) (vx: struct_point) :
+ (stt_ghost
+ unit
+ emp_inames
+ (Pulse.Lib.Reference.pts_to x #p vx)
+ (fun _ ->
+ ((struct_point__aux_raw_unfolded x p) **
+ (Pulse.Lib.Reference.pts_to (struct_point__x_1 x) #p vx.struct_point__x) **
+ (Pulse.Lib.Reference.pts_to (struct_point__y_1 x) #p vx.struct_point__y))))
+[@@pulse_intro]
+assume val struct_point__aux_raw_fold (x: (ref struct_point)) (#p: perm) v_x v_y :
+ (stt_ghost
+ unit
+ emp_inames
+ ((struct_point__aux_raw_unfolded x p) **
+ (Pulse.Lib.Reference.pts_to (struct_point__x_1 x) #p v_x) **
+ (Pulse.Lib.Reference.pts_to (struct_point__y_1 x) #p v_y))
+ (fun _ -> (Pulse.Lib.Reference.pts_to x #p { struct_point__x=v_x; struct_point__y=v_y; })))
+[@@pulse_intro]
+assume val struct_point__aux_raw_fold_uninit (x: (ref struct_point)) :
+ (stt_ghost
+ unit
+ emp_inames
+ ((struct_point__aux_raw_unfolded x 1.0R) **
+ (Pulse.Lib.Reference.pts_to_uninit (struct_point__x_1 x)) **
+ (Pulse.Lib.Reference.pts_to_uninit (struct_point__y_1 x)))
+ (fun _ -> (Pulse.Lib.Reference.pts_to_uninit x)))
+assume val struct_point__aux_raw_unfold_uninit (x: (ref struct_point)) :
+ (stt_ghost
+ unit
+ emp_inames
+ (Pulse.Lib.Reference.pts_to_uninit x)
+ (fun _ ->
+ ((struct_point__aux_raw_unfolded x 1.0R) **
+ (Pulse.Lib.Reference.pts_to_uninit (struct_point__x_1 x)) **
+ (Pulse.Lib.Reference.pts_to_uninit (struct_point__y_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_point__get_x (x: (ref struct_point)) (#p: perm) :
+ (stt_atomic
+ (ref Typedef_uint32_t.ty_uint32_t)
+ #PulseCore.Observability.Neutral
+ emp_inames
+ (struct_point__aux_raw_unfolded x p)
+ (fun vx' ->
+ ((struct_point__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_point__x_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_point__get_y (x: (ref struct_point)) (#p: perm) :
+ (stt_atomic
+ (ref Typedef_uint32_t.ty_uint32_t)
+ #PulseCore.Observability.Neutral
+ emp_inames
+ (struct_point__aux_raw_unfolded x p)
+ (fun vx' ->
+ ((struct_point__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_point__y_1 x)))))
+instance has_zero_default_struct_point : (has_zero_default struct_point) =
+ { zero_default = { struct_point__x = zero_default; struct_point__y = zero_default; } }
\ No newline at end of file
diff --git head/nullable_const_in/TranslationErrors.fst head/nullable_const_in/TranslationErrors.fst
new file mode 100644
index 0000000..bf62561
--- /dev/null
+++ head/nullable_const_in/TranslationErrors.fst
@@ -0,0 +1 @@
+module TranslationErrors
diff --git head/nullable_const_in/Typedef_PCPair.fst head/nullable_const_in/Typedef_PCPair.fst
new file mode 100644
index 0000000..54582a0
--- /dev/null
+++ head/nullable_const_in/Typedef_PCPair.fst
@@ -0,0 +1,15 @@
+module Typedef_PCPair
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_pcpair : Type = (ref Typedef_Pair.ty_pair)
+[@@pulse_eager_unfold] let predicate ty_pcpair__pred
+ ([@@@mkey] this: ty_pcpair)
+ (p: perm)
+ (val_this_0: Typedef_Pair.ty_pair) =
+ ((Pulse.Lib.Reference.pts_to this #p val_this_0) ** (Typedef_Pair.ty_pair__pred (!this) p))
+[@@pulse_eager_unfold] let predicate ty_pcpair__uninit_pred ([@@@mkey] this: ty_pcpair) =
+ ((Pulse.Lib.Reference.pts_to_uninit this))
+instance has_zero_default_ty_pcpair : (has_zero_default ty_pcpair) = { zero_default = null }
\ No newline at end of file
diff --git head/nullable_const_in/Typedef_PCPoint.fst head/nullable_const_in/Typedef_PCPoint.fst
new file mode 100644
index 0000000..9ca0c64
--- /dev/null
+++ head/nullable_const_in/Typedef_PCPoint.fst
@@ -0,0 +1,15 @@
+module Typedef_PCPoint
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_pcpoint : Type = (ref Typedef_Point.ty_point)
+[@@pulse_eager_unfold] let predicate ty_pcpoint__pred
+ ([@@@mkey] this: ty_pcpoint)
+ (p: perm)
+ (val_this_0: Typedef_Point.ty_point) =
+ ((Pulse.Lib.Reference.pts_to this #p val_this_0) ** (Typedef_Point.ty_point__pred (!this) p))
+[@@pulse_eager_unfold] let predicate ty_pcpoint__uninit_pred ([@@@mkey] this: ty_pcpoint) =
+ ((Pulse.Lib.Reference.pts_to_uninit this))
+instance has_zero_default_ty_pcpoint : (has_zero_default ty_pcpoint) = { zero_default = null }
\ No newline at end of file
diff --git head/nullable_const_in/Typedef_Pair.fst head/nullable_const_in/Typedef_Pair.fst
new file mode 100644
index 0000000..eff5c22
--- /dev/null
+++ head/nullable_const_in/Typedef_Pair.fst
@@ -0,0 +1,12 @@
+module Typedef_Pair
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_pair : Type = Struct_Pair.struct_pair
+[@@pulse_eager_unfold] let predicate ty_pair__pred ([@@@mkey] this: ty_pair) (p: perm) =
+ ((Struct_Pair.struct_pair__pred this p))
+[@@pulse_eager_unfold] let predicate ty_pair__uninit_pred ([@@@mkey] this: ty_pair) =
+ ((Struct_Pair.struct_pair__uninit_pred this))
+instance has_zero_default_ty_pair : (has_zero_default ty_pair) = { zero_default = zero_default }
\ No newline at end of file
diff --git head/nullable_const_in/Typedef_Point.fst head/nullable_const_in/Typedef_Point.fst
new file mode 100644
index 0000000..0b3e26e
--- /dev/null
+++ head/nullable_const_in/Typedef_Point.fst
@@ -0,0 +1,12 @@
+module Typedef_Point
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_point : Type = Struct_Point.struct_point
+[@@pulse_eager_unfold] let predicate ty_point__pred ([@@@mkey] this: ty_point) (p: perm) =
+ ((Struct_Point.struct_point__pred this p))
+[@@pulse_eager_unfold] let predicate ty_point__uninit_pred ([@@@mkey] this: ty_point) =
+ ((Struct_Point.struct_point__uninit_pred this))
+instance has_zero_default_ty_point : (has_zero_default ty_point) = { zero_default = zero_default }
\ No newline at end of file
diff --git head/nullable_const_in/Typedef___uint32_t.fst head/nullable_const_in/Typedef___uint32_t.fst
new file mode 100644
index 0000000..b9a5b44
--- /dev/null
+++ head/nullable_const_in/Typedef___uint32_t.fst
@@ -0,0 +1,13 @@
+module Typedef___uint32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty___uint32_t : Type = UInt32.t
+[@@pulse_eager_unfold] let predicate ty___uint32_t__pred ([@@@mkey] this: ty___uint32_t) (p: perm) =
+ emp
+[@@pulse_eager_unfold] let predicate ty___uint32_t__uninit_pred ([@@@mkey] this: ty___uint32_t) =
+ emp
+instance has_zero_default_ty___uint32_t : (has_zero_default ty___uint32_t) =
+ { zero_default = (UInt32.uint_to_t 0) }
\ No newline at end of file
diff --git head/nullable_const_in/Typedef_uint32_t.fst head/nullable_const_in/Typedef_uint32_t.fst
new file mode 100644
index 0000000..aa0f488
--- /dev/null
+++ head/nullable_const_in/Typedef_uint32_t.fst
@@ -0,0 +1,13 @@
+module Typedef_uint32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_uint32_t : Type = Typedef___uint32_t.ty___uint32_t
+[@@pulse_eager_unfold] let predicate ty_uint32_t__pred ([@@@mkey] this: ty_uint32_t) (p: perm) =
+ ((Typedef___uint32_t.ty___uint32_t__pred this p))
+[@@pulse_eager_unfold] let predicate ty_uint32_t__uninit_pred ([@@@mkey] this: ty_uint32_t) =
+ ((Typedef___uint32_t.ty___uint32_t__uninit_pred this))
+instance has_zero_default_ty_uint32_t : (has_zero_default ty_uint32_t) =
+ { zero_default = zero_default }
\ No newline at end of file
diff --git head/nullable_const_in/diagnostics.json head/nullable_const_in/diagnostics.json
new file mode 100644
index 0000000..9e26dfe
--- /dev/null
+++ head/nullable_const_in/diagnostics.json
@@ -0,0 +1 @@
+{}
\ No newline at end of file
diff --git base/nullable_out/Func_forward_neither.fst head/nullable_out/Func_forward_neither.fst
index b7c8b77..1ec8fca 100644
--- base/nullable_out/Func_forward_neither.fst
+++ head/nullable_out/Func_forward_neither.fst
@@ -9,7 +9,9 @@ divergent fn func_forward_neither (var_src: (ref Typedef_uint64_t.ty_uint64_t))
returns return_1 : unit
{
let mut var_src = var_src;
- (Func_opt_write_many.func_opt_write_many (!var_src) null null);
- Pulse.Lib.C.Nullable.elim_null_ref null;
- Pulse.Lib.C.Nullable.elim_null_ref null;
+ let __pal_null_8 = Pulse.Lib.C.Nullable.null_ref (Typedef_uint64_t.ty_uint64_t);
+ let __pal_null_9 = Pulse.Lib.C.Nullable.null_ref (Typedef_uint64_t.ty_uint64_t);
+ (Func_opt_write_many.func_opt_write_many (!var_src) __pal_null_8 __pal_null_9);
+ Pulse.Lib.C.Nullable.elim_null_ref __pal_null_8;
+ Pulse.Lib.C.Nullable.elim_null_ref __pal_null_9;
}
\ No newline at end of file
diff --git base/nullable_out/Func_forward_one.fst head/nullable_out/Func_forward_one.fst
index 8217590..4e2f59b 100644
--- base/nullable_out/Func_forward_one.fst
+++ head/nullable_out/Func_forward_one.fst
@@ -19,7 +19,8 @@ divergent fn func_forward_one
let mut var_src = var_src;
let mut var_dst = var_dst;
Pulse.Lib.Reference.pts_to_uninit_not_null ((!var_dst));
- (Func_opt_write_many.func_opt_write_many (!var_src) (!var_dst) null);
+ let __pal_null_6 = Pulse.Lib.C.Nullable.null_ref (Typedef_uint64_t.ty_uint64_t);
+ (Func_opt_write_many.func_opt_write_many (!var_src) (!var_dst) __pal_null_6);
Pulse.Lib.C.Nullable.elim_unless_null_ref ((!var_dst));
- Pulse.Lib.C.Nullable.elim_null_ref null;
+ Pulse.Lib.C.Nullable.elim_null_ref __pal_null_6;
}
\ No newline at end of file
diff --git base/nullable_out/Func_forward_optional.fst head/nullable_out/Func_forward_optional.fst
index f3c1422..d7bfb5c 100644
--- base/nullable_out/Func_forward_optional.fst
+++ head/nullable_out/Func_forward_optional.fst
@@ -20,6 +20,7 @@ divergent fn func_forward_optional
{
let mut var_src = var_src;
let mut var_dst = var_dst;
- (Func_opt_write_many.func_opt_write_many (!var_src) (!var_dst) null);
- Pulse.Lib.C.Nullable.elim_null_ref null;
+ let __pal_null_10 = Pulse.Lib.C.Nullable.null_ref (Typedef_uint64_t.ty_uint64_t);
+ (Func_opt_write_many.func_opt_write_many (!var_src) (!var_dst) __pal_null_10);
+ Pulse.Lib.C.Nullable.elim_null_ref __pal_null_10;
}
\ No newline at end of file
diff --git base/nullable_out/Func_forward_other.fst head/nullable_out/Func_forward_other.fst
index 287fa54..cc2823b 100644
--- base/nullable_out/Func_forward_other.fst
+++ head/nullable_out/Func_forward_other.fst
@@ -18,8 +18,9 @@ divergent fn func_forward_other
{
let mut var_src = var_src;
let mut var_dst = var_dst;
+ let __pal_null_7 = Pulse.Lib.C.Nullable.null_ref (Typedef_uint64_t.ty_uint64_t);
Pulse.Lib.Reference.pts_to_uninit_not_null ((!var_dst));
- (Func_opt_write_many.func_opt_write_many (!var_src) null (!var_dst));
- Pulse.Lib.C.Nullable.elim_null_ref null;
+ (Func_opt_write_many.func_opt_write_many (!var_src) __pal_null_7 (!var_dst));
+ Pulse.Lib.C.Nullable.elim_null_ref __pal_null_7;
Pulse.Lib.C.Nullable.elim_unless_null_ref ((!var_dst));
}
\ No newline at end of file
diff --git base/nullable_out/Func_via_local.fst head/nullable_out/Func_via_local.fst
index dba0795..07c1c80 100644
--- base/nullable_out/Func_via_local.fst
+++ head/nullable_out/Func_via_local.fst
@@ -20,8 +20,9 @@ divergent fn func_via_local
let mut var_dst = var_dst;
let mut var_tmp : Typedef_uint64_t.ty_uint64_t;
Pulse.Lib.Reference.pts_to_uninit_not_null (var_tmp);
- (Func_opt_write_many.func_opt_write_many (!var_src) var_tmp null);
+ let __pal_null_11 = Pulse.Lib.C.Nullable.null_ref (Typedef_uint64_t.ty_uint64_t);
+ (Func_opt_write_many.func_opt_write_many (!var_src) var_tmp __pal_null_11);
Pulse.Lib.C.Nullable.elim_unless_null_ref (var_tmp);
- Pulse.Lib.C.Nullable.elim_null_ref null;
+ Pulse.Lib.C.Nullable.elim_null_ref __pal_null_11;
(!var_dst) := (!var_tmp);
}
\ No newline at end of file
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part of the upstreaming of
nswamy/pal-c-project-integration(PR29 of 35 PRs) — seePR_PLAN.mdon that branch for the whole plan and the dependency graph.Base:
nswamy/pal-pr23-const-typedef— a stacked PR. It depends onnswamy/pal-pr23-const-typedef,nswamy/pal-pr28-nullable-caller-transfer, so only the commits listed below are its own; it will be retargeted atmainonce its parents land.A call declining several
_nullableoutputs passed the sameNULLfor each, so the guardsdiffered only in the resource they carry — which is exactly the implicit
elim_null_refmust recover by matching. With more than one in scope the match is ambiguous and the whole
thing surfaces as "Could not solve typeclass constraint
has_is_null", naming a typeclassthat appears nowhere in the C. Splits the guards at the pointer instead:
null_refreturns a null pointer bound to a name, one per declined output. The second commit lets a
call site decline an optional const input, whose guarded resource names the permission
and pointee the caller handed in; a declining caller holds nothing to solve those against,
so the guard —
emp, the pointer being null — is written down at the call site with nometavariables left in it. Callers previously worked around this by declaring such
parameters mutable, which locks out any caller holding only a fraction of the argument.
Commits
Testing
Verified:
make rust lib,test/check-template.sh,cargo fmt --check,clang-format --dry-run --Werror, and F* verification oftest/array_typedef_pointer,test/const_typedef,test/nullable_const_in,test/nullable_out,test/nullable_out_struct.