Skip to content

Commit 8690a29

Browse files
tahina-protahina-pro
committed
allow const source buffers for memcpy
this commit should go hand-in-hand with FStarLang/karamel#537
1 parent 6e07a5d commit 8690a29

13 files changed

+153
-99
lines changed

‎lib/pulse/lib/Pulse.Lib.ArrayPtr.fst‎

Lines changed: 0 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -227,37 +227,3 @@ fn join (#t: Type) (s1: ptr t) (#p: perm) (#v1: Seq.seq t) (s2: ptr t) (#v2: Seq
227227
A.pts_to_range_join s1.base (SZ.v s1.offset) (SZ.v s1.offset + Seq.length v1) (SZ.v s1.offset + Seq.length v1 + Seq.length v2);
228228
fold_pts_to s1 #p (Seq.append v1 v2)
229229
}
230-
231-
module R = Pulse.Lib.Reference
232-
233-
fn memcpy
234-
(#t:Type0) (#p0:perm)
235-
(src:ptr t) (idx_src: SZ.t)
236-
(dst:ptr t) (idx_dst: SZ.t)
237-
(len: SZ.t)
238-
(#s0:Ghost.erased (Seq.seq t) { SZ.v idx_src + SZ.v len <= Seq.length s0 })
239-
(#s1:Ghost.erased (Seq.seq t) { SZ.v idx_dst + SZ.v len <= Seq.length s1 })
240-
requires pts_to src #p0 s0 ** pts_to dst s1
241-
ensures pts_to src #p0 s0 **
242-
pts_to dst (Seq.slice s0 0 (SZ.v len) `Seq.append` Seq.slice s1 (SZ.v len) (Seq.length s1))
243-
{
244-
let mut i = 0sz;
245-
while (let vi = !i; SZ.lt vi len)
246-
invariant b. exists* s1' vi.
247-
R.pts_to i vi **
248-
pts_to src #p0 s0 **
249-
pts_to dst s1' **
250-
pure (b == SZ.lt vi len /\ SZ.lte vi len /\
251-
Seq.length s1' == Seq.length s1 /\
252-
forall (j:nat). j < Seq.length s1' ==>
253-
Seq.index s1' j == (if j < SZ.v vi then Seq.index s0 j else Seq.index s1 j))
254-
{
255-
let vi = !i;
256-
let x = src.(vi);
257-
dst.(vi) <- x;
258-
i := SZ.add vi 1sz;
259-
};
260-
with s1'. assert pts_to dst s1';
261-
assert pure (s1' `Seq.equal`
262-
(Seq.slice s0 0 (SZ.v len) `Seq.append` Seq.slice s1 (SZ.v len) (Seq.length s1)))
263-
}

‎lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti‎

Lines changed: 0 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -129,14 +129,3 @@ val ghost_split (#t: Type) (s: ptr t) (#p: perm) (i: SZ.t)
129129
val join (#t: Type) (s1: ptr t) (#p: perm) (#v1: Seq.seq t) (s2: ptr t) (#v2: Seq.seq t) : stt_ghost unit emp_inames
130130
(pts_to s1 #p v1 ** pts_to s2 #p v2 ** pure (adjacent s1 (Seq.length v1) s2))
131131
(fun _ -> pts_to s1 #p (Seq.append v1 v2))
132-
133-
val memcpy
134-
(#t:Type0) (#p0:perm)
135-
(src:ptr t) (idx_src: SZ.t)
136-
(dst:ptr t) (idx_dst: SZ.t)
137-
(len: SZ.t)
138-
(#s0:Ghost.erased (Seq.seq t) { SZ.v idx_src + SZ.v len <= Seq.length s0 })
139-
(#s1:Ghost.erased (Seq.seq t) { SZ.v idx_dst + SZ.v len <= Seq.length s1 })
140-
: stt unit
141-
(pts_to src #p0 s0 ** pts_to dst s1)
142-
(fun _ -> pts_to src #p0 s0 ** pts_to dst (Seq.slice s0 0 (SZ.v len) `Seq.append` Seq.slice s1 (SZ.v len) (Seq.length s1)))

‎lib/pulse/lib/Pulse.Lib.ConstArrayPtr.fst‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,3 +45,37 @@ let split #t s #p i #v = AP.split #t s #p i #v
4545
let ghost_split #t s #p i #v = AP.ghost_split #t s #p i #v
4646

4747
let join #t s1 #p #v1 s2 #v2 = AP.join #t s1 #p #v1 s2 #v2
48+
49+
module R = Pulse.Lib.Reference
50+
51+
fn memcpy
52+
(#t:Type0) (#p0:perm)
53+
(src:ptr t) (idx_src: SZ.t)
54+
(dst:ptr t) (idx_dst: SZ.t)
55+
(len: SZ.t)
56+
(#s0:Ghost.erased (Seq.seq t) { SZ.v idx_src + SZ.v len <= Seq.length s0 })
57+
(#s1:Ghost.erased (Seq.seq t) { SZ.v idx_dst + SZ.v len <= Seq.length s1 })
58+
requires pts_to src #p0 s0 ** pts_to dst s1
59+
ensures pts_to src #p0 s0 **
60+
pts_to dst (Seq.slice s0 0 (SZ.v len) `Seq.append` Seq.slice s1 (SZ.v len) (Seq.length s1))
61+
{
62+
let mut i = 0sz;
63+
while (let vi = !i; SZ.lt vi len)
64+
invariant b. exists* s1' vi.
65+
R.pts_to i vi **
66+
pts_to src #p0 s0 **
67+
pts_to dst s1' **
68+
pure (b == SZ.lt vi len /\ SZ.lte vi len /\
69+
Seq.length s1' == Seq.length s1 /\
70+
forall (j:nat). j < Seq.length s1' ==>
71+
Seq.index s1' j == (if j < SZ.v vi then Seq.index s0 j else Seq.index s1 j))
72+
{
73+
let vi = !i;
74+
let x = src.(vi);
75+
AP.op_Array_Assignment dst vi x;
76+
i := SZ.add vi 1sz;
77+
};
78+
with s1'. assert pts_to dst s1';
79+
assert pure (s1' `Seq.equal`
80+
(Seq.slice s0 0 (SZ.v len) `Seq.append` Seq.slice s1 (SZ.v len) (Seq.length s1)))
81+
}

‎lib/pulse/lib/Pulse.Lib.ConstArrayPtr.fsti‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -119,3 +119,14 @@ val ghost_split (#t: Type) (s: ptr t) (#p: perm) (i: SZ.t)
119119
val join (#t: Type) (s1: ptr t) (#p: perm) (#v1: Seq.seq t) (s2: ptr t) (#v2: Seq.seq t) : stt_ghost unit emp_inames
120120
(pts_to s1 #p v1 ** pts_to s2 #p v2 ** pure (adjacent s1 (Seq.length v1) s2))
121121
(fun _ -> pts_to s1 #p (Seq.append v1 v2))
122+
123+
val memcpy
124+
(#t:Type0) (#p0:perm)
125+
(src:ptr t) (idx_src: SZ.t)
126+
(dst:AP.ptr t) (idx_dst: SZ.t)
127+
(len: SZ.t)
128+
(#s0:Ghost.erased (Seq.seq t) { SZ.v idx_src + SZ.v len <= Seq.length s0 })
129+
(#s1:Ghost.erased (Seq.seq t) { SZ.v idx_dst + SZ.v len <= Seq.length s1 })
130+
: stt unit
131+
(pts_to src #p0 s0 ** pts_to dst s1)
132+
(fun _ -> pts_to src #p0 s0 ** pts_to dst (Seq.slice s0 0 (SZ.v len) `Seq.append` Seq.slice s1 (SZ.v len) (Seq.length s1)))

‎lib/pulse/lib/Pulse.Lib.MutableSlice.fst‎

Lines changed: 45 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ module Pulse.Lib.MutableSlice
1818
#lang-pulse
1919

2020
module AP = Pulse.Lib.ArrayPtr
21+
module Trade = Pulse.Lib.Trade.Util
2122

2223
noeq
2324
type slice t = {
@@ -159,6 +160,41 @@ ensures
159160
fold_pts_to s #p v
160161
}
161162

163+
module CAP = Pulse.Lib.ConstArrayPtr
164+
165+
fn to_slice
166+
(#t: Type) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t))
167+
requires
168+
pts_to s #p v
169+
returns res: S.slice t
170+
ensures
171+
pts_to res #p v ** Trade.trade (pts_to res #p v) (pts_to s #p v)
172+
{
173+
let len = len s;
174+
pts_to_len s;
175+
let a = slice_to_arrayptr_intro s;
176+
ghost fn aux (_: unit)
177+
requires slice_to_arrayptr s a ** pts_to a #p v
178+
ensures pts_to s #p v
179+
{
180+
slice_to_arrayptr_elim a;
181+
};
182+
Trade.intro _ _ _ aux;
183+
let ca = CAP.from_arrayptr a;
184+
Trade.trans _ _ (pts_to s #p v);
185+
let res = S.arrayptr_to_slice_intro ca len;
186+
S.pts_to_len res;
187+
ghost fn aux2 (_: unit)
188+
requires S.arrayptr_to_slice ca res ** pts_to res #p v
189+
ensures pts_to ca #p v
190+
{
191+
S.arrayptr_to_slice_elim res
192+
};
193+
Trade.intro _ _ _ aux2;
194+
Trade.trans _ _ (pts_to s #p v);
195+
res
196+
}
197+
162198
fn op_Array_Access
163199
(#t: Type)
164200
(a: slice t)
@@ -324,19 +360,21 @@ fn subslice #t (s: slice t) #p (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <= S
324360
}
325361

326362
fn copy
327-
(#t: Type) (dst: slice t) (#p: perm) (src: slice t) (#v: Ghost.erased (Seq.seq t))
363+
(#t: Type) (dst: slice t) (#p: perm) (src: S.slice t) (#v: Ghost.erased (Seq.seq t))
328364
requires
329-
(exists* v_dst . pts_to dst v_dst ** pts_to src #p v ** pure (len src == len dst))
365+
(exists* v_dst . pts_to dst v_dst ** pts_to src #p v ** pure (S.len src == len dst))
330366
ensures
331367
(pts_to dst v ** pts_to src #p v)
332368
{
333369
with v_dst . assert (pts_to dst v_dst);
334370
unfold_pts_to dst v_dst;
335-
unfold_pts_to src #p v;
336-
AP.memcpy src.elt 0sz dst.elt 0sz src.len;
337-
fold_pts_to src #p v;
371+
S.pts_to_len src;
372+
let slen = S.len src;
373+
let ssrc = S.slice_to_arrayptr_intro src;
374+
CAP.memcpy ssrc 0sz dst.elt 0sz slen;
375+
S.slice_to_arrayptr_elim ssrc;
338376
assert pure (v `Seq.equal`
339-
Seq.append (Seq.slice v 0 (SZ.v src.len))
340-
(Seq.slice v_dst (SZ.v src.len) (Seq.length v_dst)));
377+
Seq.append (Seq.slice v 0 (SZ.v (S.len src)))
378+
(Seq.slice v_dst (SZ.v (S.len src)) (Seq.length v_dst)));
341379
fold_pts_to dst v
342380
}

‎lib/pulse/lib/Pulse.Lib.MutableSlice.fsti‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,8 @@ open FStar.Tactics.V2
1919
open Pulse.Lib.Pervasives
2020
module SZ = FStar.SizeT
2121
module A = Pulse.Lib.Array
22+
module S = Pulse.Lib.Slice
23+
module Trade = Pulse.Lib.Trade
2224

2325
val slice ([@@@strictly_positive] elt: Type0) : Type0
2426

@@ -80,6 +82,12 @@ val slice_to_arrayptr_elim (#t: Type) (a: AP.ptr t) (#p: perm) (#v: Seq.seq t) (
8082

8183
(* END C only *)
8284

85+
val to_slice
86+
(#t: Type) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t))
87+
: stt (S.slice t)
88+
(pts_to s #p v)
89+
(fun res -> pts_to res #p v ** Trade.trade (pts_to res #p v) (pts_to s #p v))
90+
8391
(* Written x.(i) *)
8492
val op_Array_Access
8593
(#t: Type)
@@ -163,6 +171,6 @@ val subslice #t (s: slice t) #p (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <=
163171
stt (slice t) (pts_to s #p v)
164172
fun res -> pts_to res #p (Seq.slice v (SZ.v i) (SZ.v j)) ** subslice_rest res s p i j v
165173

166-
val copy (#t: Type) (dst: slice t) (#p: perm) (src: slice t) (#v: Ghost.erased (Seq.seq t)) : stt unit
167-
(exists* v_dst . pts_to dst v_dst ** pts_to src #p v ** pure (len src == len dst))
174+
val copy (#t: Type) (dst: slice t) (#p: perm) (src: S.slice t) (#v: Ghost.erased (Seq.seq t)) : stt unit
175+
(exists* v_dst . pts_to dst v_dst ** pts_to src #p v ** pure (S.len src == len dst))
168176
(fun _ -> pts_to dst v ** pts_to src #p v)

‎lib/pulse/lib/Pulse.Lib.Slice.fst‎

Lines changed: 0 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -160,39 +160,6 @@ ensures
160160
fold_pts_to s #p v
161161
}
162162

163-
fn from_mutable_slice
164-
(#t: Type) (s: MS.slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t))
165-
requires
166-
pts_to s #p v
167-
returns res: slice t
168-
ensures
169-
pts_to res #p v ** Trade.trade (pts_to res #p v) (pts_to s #p v)
170-
{
171-
let len = MS.len s;
172-
MS.pts_to_len s;
173-
let a = MS.slice_to_arrayptr_intro s;
174-
ghost fn aux (_: unit)
175-
requires MS.slice_to_arrayptr s a ** pts_to a #p v
176-
ensures pts_to s #p v
177-
{
178-
MS.slice_to_arrayptr_elim a;
179-
};
180-
Trade.intro _ _ _ aux;
181-
let ca = AP.from_arrayptr a;
182-
Trade.trans _ _ (pts_to s #p v);
183-
let res = arrayptr_to_slice_intro ca len;
184-
pts_to_len res;
185-
ghost fn aux2 (_: unit)
186-
requires arrayptr_to_slice ca res ** pts_to res #p v
187-
ensures pts_to ca #p v
188-
{
189-
arrayptr_to_slice_elim res
190-
};
191-
Trade.intro _ _ _ aux2;
192-
Trade.trans _ _ (pts_to s #p v);
193-
res
194-
}
195-
196163
fn op_Array_Access
197164
(#t: Type)
198165
(a: slice t)

‎lib/pulse/lib/Pulse.Lib.Slice.fsti‎

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@ open Pulse.Lib.Pervasives
2020
module SZ = FStar.SizeT
2121
module A = Pulse.Lib.Array
2222
module Trade = Pulse.Lib.Trade
23-
module MS = Pulse.Lib.MutableSlice
2423

2524
val slice ([@@@strictly_positive] elt: Type0) : Type0
2625

@@ -82,12 +81,6 @@ val slice_to_arrayptr_elim (#t: Type) (a: AP.ptr t) (#p: perm) (#v: Seq.seq t) (
8281

8382
(* END C only *)
8483

85-
val from_mutable_slice
86-
(#t: Type) (s: MS.slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t))
87-
: stt (slice t)
88-
(pts_to s #p v)
89-
(fun res -> pts_to res #p v ** Trade.trade (pts_to res #p v) (pts_to s #p v))
90-
9184
(* Written x.(i) *)
9285
val op_Array_Access
9386
(#t: Type)

‎pulse2rust/src/Pulse2Rust.Extract.fst‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -655,6 +655,7 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr =
655655
| S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, e::_)
656656
when S.string_of_mlpath p = "Pulse.Lib.Slice.from_array"
657657
|| S.string_of_mlpath p = "Pulse.Lib.MutableSlice.from_array"
658+
|| S.string_of_mlpath p = "Pulse.Lib.MutableSlice.to_slice"
658659
->
659660
extract_mlexpr g e
660661
| S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, e::_::i::_)

‎src/extraction/ExtractPulse.fst‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -141,6 +141,7 @@ let pulse_translate_expr : translate_expr_t = fun env e ->
141141
| MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ x; _p; _w ])
142142
when string_of_mlpath p = "Pulse.Lib.ArrayPtr.from_array"
143143
|| string_of_mlpath p = "Pulse.Lib.ConstArrayPtr.from_array"
144+
|| string_of_mlpath p = "Pulse.Lib.ConstArrayPtr.from_arrayptr"
144145
->
145146
translate_expr env x
146147

@@ -155,7 +156,7 @@ let pulse_translate_expr : translate_expr_t = fun env e ->
155156
EBufWrite (translate_expr env e, translate_expr env i, translate_expr env v)
156157

157158
| MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _; e1; e2; e3; e4; e5; _; _ ])
158-
when string_of_mlpath p = "Pulse.Lib.ArrayPtr.memcpy" ->
159+
when string_of_mlpath p = "Pulse.Lib.ConstArrayPtr.memcpy" ->
159160
EBufBlit (translate_expr env e1, translate_expr env e2, translate_expr env e3, translate_expr env e4, translate_expr env e5)
160161

161162
| MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ b ])

0 commit comments

Comments
 (0)