lang.v 44.5 KB
Newer Older
Michael Sammler's avatar
Michael Sammler committed
1
2
3
From iris.program_logic Require Export language ectx_language ectxi_language.
From stdpp Require Export strings.
From stdpp Require Import gmap list.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
4
From refinedc.lang Require Export base byte layout int_type.
Michael Sammler's avatar
Michael Sammler committed
5
6
7
8
Set Default Proof Using "Type".

Open Scope Z_scope.

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
9
(** * Locations *)
10

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
11
12
13
Declare Scope loc_scope.
Delimit Scope loc_scope with L.
Open Scope loc_scope.
14

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
15
16
(** Physical address. *)
Definition addr := Z.
Michael Sammler's avatar
Michael Sammler committed
17

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
18
19
20
(** Allocation identifier (unique to an allocation). *)
Definition alloc_id := Z.
Definition dummy_alloc_id : alloc_id := 0.
21

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
22
23
24
(** Memory location. *)
Definition loc : Set := option alloc_id * addr.
Bind Scope loc_scope with loc.
25

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
26
27
28
29
Definition shift_loc (l : loc) (z : Z) : loc := (l.1, l.2 + z).
Notation "l +ₗ z" := (shift_loc l%L z%Z)
  (at level 50, left associativity) : loc_scope.
Typeclasses Opaque shift_loc.
30

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
31
32
33
34
Definition offset_loc (l : loc) (ly : layout) (z : Z) : loc := (l + ly.(ly_size) * z).
Notation "l 'offset{' ly '}ₗ' z" := (offset_loc l%L ly z%Z)
  (at level 50, format "l  'offset{' ly '}ₗ'  z", left associativity) : loc_scope.
Typeclasses Opaque offset_loc.
35

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
36
37
38
39
Definition aligned_to (l : loc) (n : nat) : Prop := (n | l.2).
Notation "l `aligned_to` n" := (aligned_to l n) (at level 50) : stdpp_scope.
Arguments aligned_to : simpl never.
Typeclasses Opaque aligned_to.
40

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
41
42
43
44
Definition has_layout_loc (l : loc) (ly : layout) : Prop := l `aligned_to` ly_align ly.
Notation "l `has_layout_loc` n" := (has_layout_loc l n) (at level 50) : stdpp_scope.
Arguments has_layout_loc : simpl never.
Typeclasses Opaque has_layout_loc.
45

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
46
47
48
49
Section loc_lemmas.
  (*+ Lemmas about [shift_loc] and [offset_loc] *)
  Lemma shift_loc_assoc l n1 n2 : l + n1 + n2 = l + (n1 + n2).
  Proof. rewrite /shift_loc /=. f_equal. lia. Qed.
50

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
51
52
  Lemma shift_loc_0 l : l + 0 = l.
  Proof. destruct l as [??]. by rewrite /shift_loc Z.add_0_r. Qed.
53

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
54
55
  Lemma shift_loc_assoc_nat l (n1 n2 : nat) : l + n1 + n2 = l + (n1 + n2)%nat.
  Proof. rewrite /shift_loc /=. f_equal. lia. Qed.
56

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
57
58
  Lemma shift_loc_0_nat l : l + 0%nat = l.
  Proof. have: Z.of_nat 0%nat = 0 by lia. move => ->. apply shift_loc_0. Qed.
59

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
60
61
  Lemma shift_loc_S l n: l + S n = (l + 1%nat + n).
  Proof. by rewrite shift_loc_assoc_nat. Qed.
Michael Sammler's avatar
Michael Sammler committed
62

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
63
64
  Lemma shift_loc_inj1 l1 l2 n : l1 + n = l2 + n  l1 = l2.
  Proof. destruct l1, l2. case => -> ?. f_equal. lia. Qed.
Michael Sammler's avatar
Michael Sammler committed
65

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
66
67
  Global Instance shift_loc_inj2 l : Inj (=) (=) (shift_loc l).
  Proof. destruct l as [b o]; intros n n' [=?]; lia. Qed.
68

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
69
70
  Lemma shift_loc_block l n : (l + n).1 = l.1.
  Proof. done. Qed.
71

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
72
73
  Lemma offset_loc_0 l ly : l offset{ly} 0 = l.
  Proof. by rewrite /offset_loc Z.mul_0_r shift_loc_0. Qed.
74

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
75
76
  Lemma offset_loc_S l ly n : l offset{ly} S n = (l offset{ly} 1) offset{ly} n.
  Proof. destruct l. rewrite /offset_loc /shift_loc /=. f_equal. lia. Qed.
77

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
78
79
  Lemma offset_loc_1 l ly : l offset{ly} 1%nat = (l + ly.(ly_size)).
  Proof. destruct l. rewrite /offset_loc /shift_loc /=. f_equal. lia. Qed.
80

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
81
82
  Lemma offset_loc_sz1 ly l n : ly.(ly_size) = 1%nat  l offset{ly} n = l + n.
  Proof. rewrite /offset_loc => ->. f_equal. lia. Qed.
83

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
84
85
86
87
88
89
  (*+ Lemmas about [aligned_to] and [has_layout_loc] *)
  Lemma ly_with_align_aligned_to l m n:
    l `aligned_to` n 
    is_power_of_two n 
    l `has_layout_loc` ly_with_align m n.
  Proof. move => ??. by rewrite /has_layout_loc ly_align_ly_with_align keep_factor2_is_power_of_two. Qed.
90

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
91
92
93
  Lemma has_layout_loc_trans l ly1 ly2 :
    l `has_layout_loc` ly2  (ly1.(ly_align_log)  ly2.(ly_align_log))%nat  l `has_layout_loc` ly1.
  Proof. rewrite /has_layout_loc/aligned_to => Hl ?. etrans;[|by apply Hl]. by apply Zdivide_nat_pow. Qed.
Fengmin Zhu's avatar
Ci/bits    
Fengmin Zhu committed
94

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
95
96
97
  Lemma has_layout_loc_trans' l ly1 ly2 :
    l `has_layout_loc` ly2  (ly_align ly1  ly_align ly2)%nat  l `has_layout_loc` ly1.
  Proof. rewrite -ly_align_log_ly_align_le_iff. by apply: has_layout_loc_trans. Qed.
98

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
99
100
101
102
  Lemma has_layout_loc_1 l ly:
    ly_align ly = 1%nat 
    l `has_layout_loc` ly.
  Proof. rewrite /has_layout_loc =>  ->. by apply Z.divide_1_l. Qed.
103

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
104
105
106
  Lemma has_layout_ly_offset l (n : nat) ly:
    l `has_layout_loc` ly 
    (l + n) `has_layout_loc` ly_offset ly n.
107
  Proof.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
108
109
110
    move => Hl. apply Z.divide_add_r.
    - apply: has_layout_loc_trans => //. rewrite {1}/ly_align_log/=. destruct n; lia.
    - rewrite/ly_offset. destruct n;[by subst;apply Z.divide_0_r|]. etrans;[apply Zdivide_nat_pow, Min.le_min_r|].   by apply factor2_divide.
111
112
  Qed.

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
113
114
115
116
117
118
  Lemma has_layout_loc_ly_mult_offset l ly n:
    layout_wf ly 
    l `has_layout_loc` ly_mult ly (S n) 
    (l + ly_size ly) `has_layout_loc` ly_mult ly n.
  Proof. move => ??. rewrite /ly_mult. by apply Z.divide_add_r. Qed.

119

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
120
121
122
  Lemma aligned_to_offset l n off :
    l `aligned_to` n  (n | off)  (l + off) `aligned_to` n.
  Proof. apply Z.divide_add_r. Qed.
123

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
124
125
  Lemma aligned_to_add l (n : nat) x:
    (l + x * n) `aligned_to` n  l `aligned_to` n.
126
  Proof.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
127
128
129
130
    unfold aligned_to. destruct l => /=. rewrite Z.add_comm.
    split.
    - apply: Z.divide_add_cancel_r. by apply Z.divide_mul_r.
    - apply Z.divide_add_r. by apply Z.divide_mul_r.
131
132
  Qed.

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
133
134
  Lemma aligned_to_mult_eq l n1 n2 off:
    l `aligned_to` n2  (l + off) `aligned_to` (n1 * n2)  (n2 | off).
135
  Proof.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
136
137
    unfold aligned_to. destruct l => /= ??. apply: Z.divide_add_cancel_r => //.
    apply: (Zdivide_mult_l _ n1). by rewrite Z.mul_comm -Nat2Z.inj_mul.
138
  Qed.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
139
End loc_lemmas.
140

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
141
(** * Bytes and values stored in memory *)
142

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
143
144
145
146
147
(** Representation of a byte stored in memory. *)
Inductive mbyte : Set :=
| MByte (b : byte)
| MPtrFrag (l : loc) (n : nat)
| MPoison.
Michael Sammler's avatar
Michael Sammler committed
148

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
149
150
151
(** Representation of a value (list of bytes). *)
Definition val : Set := list mbyte.
Bind Scope val_scope with val.
152

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
153
154
155
156
Definition has_layout_val (v : val) (ly : layout) : Prop := length v = ly.(ly_size).
Notation "v `has_layout_val` n" := (has_layout_val v n) (at level 50) : stdpp_scope.
Arguments has_layout_val : simpl never.
Typeclasses Opaque has_layout_val.
157

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
158
(** * Representation of the heap *)
159

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
160
Inductive lock_state := WSt | RSt (n : nat).
161

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
162
163
164
165
166
Record heap_cell := HeapCell {
  hc_alloc_id   : alloc_id;   (** Allocation owning the cell. *)
  hc_lock_state : lock_state; (** Datarace detection stuff. *)
  hc_value      : mbyte;      (** Byte value. *)
}.
167

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
168
Definition heap := gmap addr heap_cell.
169

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
170
171
172
173
174
175
176
177
178
179
(** Predicate stating that the heap [h] contains value [v] at address [a],
and that every cell involved has an allocation identifier and a lock state
that satisfy [Paid] and [Plk] respectively. *)
Fixpoint heap_lookup (a : addr) (v : val) (Paid : alloc_id  Prop)
                       (Plk : lock_state  Prop) (h : heap) : Prop :=
  match v with
  | []     => True
  | b :: v => ( aid lk, h !! a = Some (HeapCell aid lk b)  Paid aid  Plk lk) 
              heap_lookup (Z.succ a) v Paid Plk h
  end.
180

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
(** Function writing value [v] at address [a] in heap [h]. For all involved
cells in the resulting heap, an allocation id and lock state is built using
functions [faid] and [flk] respectively. These functions receive as input
the previous value of the field (if the cell previously existed in [h]). *)
Fixpoint heap_update (a : addr) (v : val) (faid : option alloc_id  alloc_id)
                     (flk : option lock_state  lock_state) (h : heap) : heap :=
  match v with
  | []     => h
  | b :: v => let update m :=
                Some {|
                  hc_alloc_id   := faid (hc_alloc_id <$> m);
                  hc_lock_state := flk (hc_lock_state <$> m);
                  hc_value      := b;
                |}
              in
              partial_alter update a (heap_update (Z.succ a) v faid flk h)
  end.
198

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
199
200
201
Definition heap_lookup_loc (l : loc) (v : val) (Plk : lock_state  Prop)
                             (h : heap) : Prop :=
  heap_lookup l.2 v (λ aid, l.1 = Some aid) Plk h.
202

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
203
204
Definition heap_alloc (a : addr) (v : val) (aid : alloc_id) (h : heap) : heap :=
  heap_update a v (λ _, aid) (λ _, RSt 0%nat) h.
205

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
206
207
208
(** Predicate stating that the allocation [aid] is still present in heap [h]. *)
Definition heap_block_alive (h : heap) (aid : alloc_id) : Prop :=
   a, hc_alloc_id <$> h !! a = Some aid.
209

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
210
211
212
213
214
215
216
Definition heap_at (l : loc) (ly : layout) (v : val) (Plk : lock_state  Prop)
                   (h : heap) : Prop :=
  is_Some l.1  l `has_layout_loc` ly  v `has_layout_val` ly 
  heap_lookup_loc l v Plk h.

Definition heap_upd l v flk h :=
  heap_update l.2 v (λ _, default dummy_alloc_id l.1) flk h.
217

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
(** Predicate stating that the [n] first bytes from address [a] in [h] have
not been allocated. *)
Definition heap_range_free (h : heap) (a : addr) (n : nat) : Prop :=
   a', a  a' < a + n  h !! a' = None.

(** Free [n] cells starting at [a] in [h]. *)
Fixpoint heap_free (a : addr) (n : nat) (h : heap) : heap :=
  match n with
  | O   => h
  | S n => delete a (heap_free (Z.succ a) n h)
  end.

Fixpoint heap_free_list (ls : list (loc * layout)) (h : heap) : heap :=
  match ls with
  | []           => h
  | (l,ly) :: ls => heap_free l.2 ly.(ly_size) (heap_free_list ls h)
  end.

Section heap_lemmas.
  Lemma heap_lookup_inj_val a h v1 v2 Paid1 Paid2 Plk1 Plk2:
    length v1 = length v2 
    heap_lookup a v1 Paid1 Plk1 h  heap_lookup a v2 Paid2 Plk2 h  v1 = v2.
  Proof.
    elim: v1 v2 a; first by move => [|??] //.
    move => ?? IH [|??] //= ? [?] [[?[?[??]]]?] [[?[?[??]]]?]; simplify_eq.
    f_equal. by apply: IH.
  Qed.

  Lemma heap_update_ext h a v faid1 faid2 flk1 flk2:
    ( x, faid1 x = faid2 x)  ( x, flk1 x = flk2 x) 
    heap_update a v faid1 flk1 h = heap_update a v faid2 flk2 h.
  Proof.
    move => Hext1 Hext2. elim: v a => //= ?? IH ?. rewrite IH.
    apply: partial_alter_ext => ??. by rewrite Hext1 Hext2.
  Qed.

  Lemma heap_update_lookup_lt a1 a2 v faid flk h:
    a1 < a2 
    heap_update a2 v faid flk h !! a1 = h !! a1.
  Proof.
    elim: v a1 a2 => // ?? IH ???.
    rewrite lookup_partial_alter_ne; last lia. apply IH. lia.
  Qed.

  Lemma heap_free_delete h a1 a2 n :
    delete a1 (heap_free a2 n h) = heap_free a2 n (delete a1 h).
  Proof. elim: n a2 => //= ? IH ?. by rewrite delete_commute IH. Qed.

  Lemma heap_free_list_app ls1 ls2 h :
    heap_free_list (ls1 ++ ls2) h = heap_free_list ls1 (heap_free_list ls2 h).
  Proof. by elim: ls1 => //= [[??]] ? ->. Qed.

  Lemma heap_upd_ext h l v f1 f2:
    ( x, f1 x = f2 x)  heap_upd l v f1 h = heap_upd l v f2 h.
  Proof. by apply heap_update_ext. Qed.

  Lemma heap_at_inj_val l ly h v1 v2 Plk1 Plk2:
    heap_at l ly v1 Plk1 h  heap_at l ly v2 Plk2 h  v1 = v2.
  Proof.
    move => [_[?[??]]] [_[?[??]]].
    apply: heap_lookup_inj_val => //. congruence.
  Qed.

  Lemma heap_lookup_loc_inj_val  l h v v' flk1 flk2 ly:
    v `has_layout_val` ly 
    heap_lookup_loc l v flk1 h  heap_at l ly v' flk2 h  v = v'.
  Proof.
    move => ??[_[?[??]]]. apply: heap_lookup_inj_val => //. congruence.
  Qed.

  Lemma heap_upd_heap_at_id l v flk flk' h:
    heap_lookup_loc l v flk' h 
    ( st, flk (Some st) = st) 
    heap_upd l v flk h = h.
  Proof.
    rewrite /heap_upd.
    elim: v l => // ?? IH ? [[?[?[H[H1 ?]]]]?] Hlookup /=.
    assert ( l, Z.succ l.2 = (l + 1).2) as -> by done.
    rewrite IH => //. apply: partial_alter_self_alt'.
    by rewrite H Hlookup H1 /=.
  Qed.
End heap_lemmas.

(** * Allocations and heap state *)
302

303
304
305
306
307
308
Record allocation :=
  Allocation {
    alloc_start : Z; (* First valid address. *)
    alloc_end : Z;   (* One-past-the-end address. *)
  }.

309
Definition allocs := gmap alloc_id allocation.
310

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
311
312
313
314
Record heap_state := {
  hs_heap   : heap;
  hs_allocs : allocs;
}.
315

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
316
317
(** Smallest allocatble address (we reserve 0 for NULL). *)
Definition min_alloc_start : Z := 1.
318

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
319
320
321
(** Largest allocatable address (we never allocate the last byte to always
have valid one-past pointers. *)
Definition max_alloc_end : Z := 2 ^ (bytes_per_addr * bits_per_byte) - 2.
Michael Sammler's avatar
Michael Sammler committed
322

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
323
324
Definition to_allocation (off : Z) (len : nat) : allocation :=
  Allocation off (off + len).
Michael Sammler's avatar
Michael Sammler committed
325

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
326
327
Definition allocation_in_range (a : allocation) : Prop :=
  min_alloc_start  a.(alloc_start)  a.(alloc_end)  max_alloc_end.
Michael Sammler's avatar
Michael Sammler committed
328

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
329
330
331
332
333
334
335
336
337
(** The address range between [l] and [l +ₗ n] (included) is in range of the
    allocation that contains [l]. Note that we consider the 1-past-the-end
    pointer to be in range of an allocation. *)
Definition heap_state_loc_in_bounds (l : loc) (n : nat) (st : heap_state) : Prop :=
   alloc_id alloc,
    l.1 = Some alloc_id 
    st.(hs_allocs) !! alloc_id = Some alloc 
    alloc.(alloc_start)  l.2 
    l.2 + n  alloc.(alloc_end).
Michael Sammler's avatar
Michael Sammler committed
338

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
339
340
341
342
(** Checks that the location [l] is inbounds of its allocation
(one-past-the-end is allowed) and this allocation is still alive *)
Definition valid_ptr (l : loc) (st : heap_state) : Prop :=
   aid, l.1 = Some aid  heap_block_alive st.(hs_heap) aid  heap_state_loc_in_bounds l 0 st.
343

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
Inductive alloc_new_block : heap_state  loc  val  heap_state  Prop :=
| AllocNewBlock σ l aid v:
    l.1 = Some aid 
    σ.(hs_allocs) !! aid = None 
    (* TODO: is the precondition really useful? It should follow from
    the previous. *)
    ¬ heap_block_alive σ.(hs_heap) aid 
    allocation_in_range (to_allocation l.2 (length v)) 
    heap_range_free σ.(hs_heap) l.2 (length v) 
    alloc_new_block σ l v {|
      hs_heap   := heap_alloc l.2 v aid σ.(hs_heap);
      hs_allocs := <[aid := to_allocation l.2 (length v)]> σ.(hs_allocs);
    |}.

Inductive alloc_new_blocks : heap_state  list loc  list val  heap_state  Prop :=
| AllocNewBlock_nil σ :
    alloc_new_blocks σ [] [] σ
| AllocNewBlock_cons σ σ' σ'' l v ls vs :
    alloc_new_block σ l v σ' 
    alloc_new_blocks σ' ls vs σ'' 
    alloc_new_blocks σ (l :: ls) (v :: vs) σ''.

(** * Definition of the language *)

Definition label := string.
369
370
Definition var_name := string.

Michael Sammler's avatar
Michael Sammler committed
371
372
373
374
375
376
Inductive op_type : Set :=
| IntOp (i : int_type) | PtrOp.

(* see http://compcert.inria.fr/doc/html/compcert.cfrontend.Cop.html#binary_operation *)
Inductive bin_op : Set :=
| AddOp | SubOp | MulOp | DivOp | ModOp | AndOp | OrOp | XorOp | ShlOp
377
| ShrOp | EqOp | NeOp | LtOp | GtOp | LeOp | GeOp
Michael Sammler's avatar
Michael Sammler committed
378
(* Ptr is the second argument and pffset the first *)
379
| PtrOffsetOp (ly : layout) | PtrNegOffsetOp (ly : layout).
Michael Sammler's avatar
Michael Sammler committed
380
381
382
383
384
385

Inductive un_op : Set :=
| NotBoolOp | NotIntOp | NegOp | CastOp (ot : op_type).
Inductive order : Set :=
| ScOrd | Na1Ord | Na2Ord.

386
387
Section expr.
Local Unset Elimination Schemes.
Michael Sammler's avatar
Michael Sammler committed
388
389
390
391
392
Inductive expr :=
| Var (x : var_name)
| Val (v : val)
| UnOp (op : un_op) (ot : op_type) (e : expr)
| BinOp (op : bin_op) (ot1 ot2 : op_type) (e1 e2 : expr)
393
| CopyAllocId (e1 : expr) (e2 : expr)
Michael Sammler's avatar
Michael Sammler committed
394
395
| Deref (o : order) (ly : layout) (e : expr)
| CAS (ot : op_type) (e1 e2 e3 : expr)
396
| Call (f : expr) (args : list expr)
Michael Sammler's avatar
Michael Sammler committed
397
| Concat (es : list expr)
Michael Sammler's avatar
Michael Sammler committed
398
| IfE (ot : op_type) (e1 e2 e3 : expr)
Michael Sammler's avatar
Michael Sammler committed
399
400
401
| SkipE (e : expr)
| StuckE (* stuck expression *)
.
402
403
404
405
406
407
408
409
410
411
412
413
End expr.
Arguments Call _%E _%E.
Lemma expr_ind (P : expr  Prop) :
  ( (x : var_name), P (Var x)) 
  ( (v : val), P (Val v)) 
  ( (op : un_op) (ot : op_type) (e : expr), P e  P (UnOp op ot e)) 
  ( (op : bin_op) (ot1 ot2 : op_type) (e1 e2 : expr), P e1  P e2  P (BinOp op ot1 ot2 e1 e2)) 
  ( (e1 e2 : expr), P e1  P e2  P (CopyAllocId e1 e2)) 
  ( (o : order) (ly : layout) (e : expr), P e  P (Deref o ly e)) 
  ( (ot : op_type) (e1 e2 e3 : expr), P e1  P e2  P e3  P (CAS ot e1 e2 e3)) 
  ( (f : expr) (args : list expr), P f  Forall P args  P (Call f args)) 
  ( (es : list expr), Forall P es  P (Concat es)) 
Michael Sammler's avatar
Michael Sammler committed
414
  ( (ot : op_type) (e1 e2 e3 : expr), P e1  P e2  P e3  P (IfE ot e1 e2 e3)) 
415
416
417
418
419
420
421
422
423
424
425
426
427
  ( (e : expr), P e  P (SkipE e)) 
  (P StuckE) 
   (e : expr), P e.
Proof.
  move => *. generalize dependent P => P. match goal with | e : expr |- _ => revert e end.
  fix FIX 1. move => [ ^e] => ??????? Hcall Hconcat *.
  8: { apply Hcall; [ |apply Forall_true => ?]; by apply: FIX. }
  8: { apply Hconcat. apply Forall_true => ?. by apply: FIX. }
  all: auto.
Qed.

Global Instance val_inj : Inj (=) (=) Val.
Proof. by move => ?? [->]. Qed.
Michael Sammler's avatar
Michael Sammler committed
428
429
430
431
432

(** Note that there is no explicit Fork. Instead the initial state can
contain multiple threads (like a processor which has a fixed number of
hardware threads). *)
Inductive stmt :=
433
| Goto (b : label)
Michael Sammler's avatar
Michael Sammler committed
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
| Return (e : expr)
(* m: map from values of e to indices into bs, def: default *)
| Switch (it : int_type) (e : expr) (m : gmap Z nat) (bs : list stmt) (def : stmt)
| Assign (o : order) (ly : layout) (e1 e2 : expr) (s : stmt)
| SkipS (s : stmt)
| StuckS (* stuck statement *)
| ExprS (e : expr) (s : stmt)
.

Arguments Switch _%E _%E _%E.

Record function := {
  f_args : list (var_name * layout);
  f_local_vars : list (var_name * layout);
  (* TODO should we add this: f_ret : layout; ?*)
449
450
  f_code : gmap label stmt;
  f_init : label;
Michael Sammler's avatar
Michael Sammler committed
451
452
}.

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
453
(* TODO: put both function and bytes in the same heap or make pointers disjoint *)
Michael Sammler's avatar
Michael Sammler committed
454
Record state := {
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
455
  st_heap: heap_state;
Michael Sammler's avatar
Michael Sammler committed
456
457
458
  st_fntbl: gmap loc function;
}.

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
459
460
461
462
463
Definition heap_fmap (f : heap  heap) (σ : state) := {|
  st_heap := {| hs_heap := f σ.(st_heap).(hs_heap); hs_allocs := σ.(st_heap).(hs_allocs) |};
  st_fntbl := σ.(st_fntbl);
|}.

Michael Sammler's avatar
Michael Sammler committed
464
465
466
467
468
469
470
471
Record runtime_function := {
  (* locations of args and local vars are substitued in the body *)
  rf_fn : function;
  (* locations in the stack frame (locations of arguments and local
  vars allocated on Call, need to be freed by Return) *)
  rf_locs: list (loc * layout);
}.

472
473
474
475
476
477
478
479
480
481
482
483
484
485
Inductive runtime_expr :=
| Expr (e : rtexpr)
| Stmt (rf : runtime_function) (s : rtstmt)
| AllocFailed
with rtexpr :=
| RTVar (x : var_name)
| RTVal (v : val)
| RTUnOp (op : un_op) (ot : op_type) (e : runtime_expr)
| RTBinOp (op : bin_op) (ot1 ot2 : op_type) (e1 e2 : runtime_expr)
| RTCopyAllocId (e1 : runtime_expr) (e2 : runtime_expr)
| RTDeref (o : order) (ly : layout) (e : runtime_expr)
| RTCall (f : runtime_expr) (args : list runtime_expr)
| RTCAS (ot : op_type) (e1 e2 e3 : runtime_expr)
| RTConcat (es : list runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
486
| RTIfE (ot : op_type) (e1 e2 e3 : runtime_expr)
487
488
489
490
491
492
493
494
495
496
497
| RTSkipE (e : runtime_expr)
| RTStuckE
with rtstmt :=
| RTGoto (b : label)
| RTReturn (e : runtime_expr)
| RTSwitch (it : int_type) (e : runtime_expr) (m : gmap Z nat) (bs : list stmt) (def : stmt)
| RTAssign (o : order) (ly : layout) (e1 e2 : runtime_expr) (s : stmt)
| RTSkipS (s : stmt)
| RTStuckS
| RTExprS (e : runtime_expr) (s : stmt)
.
498

499
500
501
502
503
504
505
506
507
508
509
Fixpoint to_rtexpr (e : expr) : runtime_expr :=
  Expr $ match e with
  | Var x => RTVar x
  | Val v => RTVal v
  | UnOp op ot e => RTUnOp op ot (to_rtexpr e)
  | BinOp op ot1 ot2 e1 e2 => RTBinOp op ot1 ot2 (to_rtexpr e1) (to_rtexpr e2)
  | CopyAllocId e1 e2 => RTCopyAllocId (to_rtexpr e1) (to_rtexpr e2)
  | Deref o ly e => RTDeref o ly (to_rtexpr e)
  | Call f args => RTCall (to_rtexpr f) (to_rtexpr <$> args)
  | CAS ot e1 e2 e3 => RTCAS ot (to_rtexpr e1) (to_rtexpr e2) (to_rtexpr e3)
  | Concat es => RTConcat (to_rtexpr <$> es)
Michael Sammler's avatar
Michael Sammler committed
510
  | IfE ot e1 e2 e3 => RTIfE ot (to_rtexpr e1) (to_rtexpr e2) (to_rtexpr e3)
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
  | SkipE e => RTSkipE (to_rtexpr e)
  | StuckE => RTStuckE
  end.
Definition coerce_rtexpr := to_rtexpr.
Coercion coerce_rtexpr : expr >-> runtime_expr.
Arguments coerce_rtexpr : simpl never.
Definition to_rtstmt (rf : runtime_function) (s : stmt) : runtime_expr :=
  Stmt rf $ match s with
  | Goto b => RTGoto b
  | Return e => RTReturn (to_rtexpr e)
  | Switch it e m bs def => RTSwitch it (to_rtexpr e) m bs def
  | Assign o ly e1 e2 s => RTAssign o ly (to_rtexpr e1) (to_rtexpr e2) s
  | SkipS s => RTSkipS s
  | StuckS => RTStuckS
  | ExprS e s => RTExprS (to_rtexpr e) s
  end.
527

528
529
530
531
532
533
534
535
536
537
538
539
540
Global Instance to_rtexpr_inj : Inj (=) (=) to_rtexpr.
Proof.
  elim => [ ^ e1 ] [ ^ e2 ] // ?; simplify_eq => //; try naive_solver.
  - f_equal. naive_solver.
    generalize dependent e2args.
    revert select (Forall _ _). elim. by case.
    move => ????? [|??]//. naive_solver.
  - generalize dependent e2es.
    revert select (Forall _ _). elim. by case.
    move => ????? [|??]//. naive_solver.
Qed.
Global Instance to_rtstmt_inj : Inj2 (=) (=) (=) to_rtstmt.
Proof. move => ? s1 ? s2 [-> ]. elim: s1 s2 => [ ^ e1 ] [ ^ e2 ] // ?; simplify_eq => //. Qed.
Michael Sammler's avatar
Michael Sammler committed
541

542
Implicit Type (l : loc) (re : rtexpr) (v : val) (sz : nat) (h : heap) (σ : state) (ly : layout) (rs : rtstmt) (s : stmt) (sgn : signed) (rf : runtime_function).
Michael Sammler's avatar
Michael Sammler committed
543
544

(*** Relating val to logical values *)
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
545
(*+ [val_to_int] and [val_of_int] *)
Michael Sammler's avatar
Michael Sammler committed
546
547
548
549
(* we use little endian *)
Fixpoint val_to_int_go v : option Z :=
match v with
| [] => Some 0
550
| (MByte b)::v' => z  val_to_int_go v'; Some (byte_modulus * z + b.(byte_val))
Michael Sammler's avatar
Michael Sammler committed
551
552
553
| _ => None
end.
Definition val_to_int (v : val) (it : int_type) : option Z :=
554
555
  if decide (length v = bytes_per_int it) then
    z  val_to_int_go v; if it.(it_signed) && bool_decide (int_half_modulus it  z) then Some (z - int_modulus it) else Some z
Michael Sammler's avatar
Michael Sammler committed
556
557
558
559
560
  else None.

Program Fixpoint val_of_int_go (n : Z) sz : val :=
  match sz return _ with
  | O => []
561
  | S sz' => (MByte ({| byte_val := (n `mod` byte_modulus) |}))::(val_of_int_go (n / byte_modulus) sz')
Michael Sammler's avatar
Michael Sammler committed
562
  end.
563
Next Obligation. move => n. have [] := Z_mod_lt n byte_modulus => //*. lia. Qed.
Michael Sammler's avatar
Michael Sammler committed
564
565

Definition val_of_int (z : Z) (it : int_type) : option val :=
566
567
568
  if bool_decide (z  it) then
    let p := if bool_decide (z < 0) then z + int_modulus it else z in
    Some (val_of_int_go p (bytes_per_int it))
Michael Sammler's avatar
Michael Sammler committed
569
570
571
572
573
574
575
576
  else
    None.

Lemma val_of_int_go_length z sz :
  length (val_of_int_go z sz) = sz.
Proof. elim: sz z => //= ? IH ?. by f_equal. Qed.

Lemma val_to_of_int_go z sz :
577
  0  z < 2 ^ (sz * bits_per_byte) 
Michael Sammler's avatar
Michael Sammler committed
578
579
  val_to_int_go (val_of_int_go z sz) = Some z.
Proof.
580
  rewrite /bits_per_byte.
Michael Sammler's avatar
Michael Sammler committed
581
  elim: sz z => /=. 1: rewrite /Z.of_nat; move => ??; f_equal; lia.
582
  move => sz IH z [? Hlt]. rewrite IH /byte_modulus /= -?Z_div_mod_eq //.
Michael Sammler's avatar
Michael Sammler committed
583
584
585
586
587
588
  split. apply Z_div_pos => //. apply Zdiv_lt_upper_bound => //.
  rewrite Nat2Z.inj_succ -Zmult_succ_l_reverse Z.pow_add_r // in Hlt.
  lia.
Qed.

Lemma val_of_int_length z it v:
589
  val_of_int z it = Some v  length v = bytes_per_int it.
Michael Sammler's avatar
Michael Sammler committed
590
591
592
Proof. rewrite /val_of_int => Hv. case_bool_decide => //. simplify_eq. by rewrite val_of_int_go_length. Qed.

Lemma val_to_int_length v it z:
593
  val_to_int v it = Some z  length v = bytes_per_int it.
Michael Sammler's avatar
Michael Sammler committed
594
595
596
Proof. rewrite /val_to_int. by case_decide. Qed.

Lemma val_of_int_is_some it z:
597
  z  it  is_Some (val_of_int z it).
Michael Sammler's avatar
Michael Sammler committed
598
599
600
Proof. rewrite /val_of_int. case_bool_decide; by eauto. Qed.

Lemma val_of_int_in_range it z v:
601
  val_of_int z it = Some v  z  it.
Michael Sammler's avatar
Michael Sammler committed
602
603
604
Proof. rewrite /val_of_int. case_bool_decide; by eauto. Qed.

Lemma val_to_of_int z it v:
605
  val_of_int z it = Some v  val_to_int v it = Some z.
Michael Sammler's avatar
Michael Sammler committed
606
607
Proof.
  rewrite /val_of_int /val_to_int => Ht.
608
609
610
611
  destruct (bool_decide (z  it)) eqn: Hr => //. simplify_eq.
  move: Hr => /bool_decide_eq_true[Hm HM].
  have Hlen := bytes_per_int_gt_0 it.
  rewrite /max_int in HM. rewrite /min_int in Hm.
Michael Sammler's avatar
Michael Sammler committed
612
  rewrite val_of_int_go_length val_to_of_int_go /=.
613
614
615
616
617
618
619
620
621
622
623
624
  - case_decide as H => //. clear H.
    destruct (it_signed it) eqn:Hs => /=.
    + case_decide => /=; last (rewrite bool_decide_false //; lia).
      rewrite bool_decide_true; [f_equal; lia|].
      rewrite int_modulus_twice_half_modulus. move: Hm HM.
      generalize (int_half_modulus it). move => n Hm HM. lia.
    + rewrite bool_decide_false //. lia.
  - case_bool_decide as Hneg; case_match; split; try lia.
    + rewrite int_modulus_twice_half_modulus. lia.
    + rewrite /int_modulus /bits_per_int. lia.
    + rewrite /int_half_modulus in HM.
      transitivity (2 ^ (bits_per_int it -1)); first lia.
625
      rewrite /bits_per_int /bytes_per_int /bits_per_byte /=.
626
627
      apply Z.pow_lt_mono_r; try lia.
    + rewrite /int_modulus /bits_per_int in HM. lia.
Michael Sammler's avatar
Michael Sammler committed
628
629
Qed.

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
630
(*+ [val_to_loc] and [val_of_loc] *)
Michael Sammler's avatar
Michael Sammler committed
631
632
Fixpoint val_to_loc_go (v : val) (pos : nat) (l : loc) : option loc :=
  match v with
633
  | (MPtrFrag l' pos')::v' =>
Michael Sammler's avatar
Michael Sammler committed
634
    if bool_decide (pos = pos'  l = l') then
635
      if bool_decide (pos = bytes_per_addr - 1)%nat then (if v' is [] then Some l else None) else val_to_loc_go v' (S pos) l
Michael Sammler's avatar
Michael Sammler committed
636
637
638
639
640
    else None
  | _ => None
  end.
Definition val_to_loc (v : val) : option loc :=
  match v with
641
  | (MPtrFrag l 0)::v' => val_to_loc_go v' 1%nat l
Michael Sammler's avatar
Michael Sammler committed
642
643
  | _ => None
  end.
644
Definition val_of_loc (l : loc) : val := MPtrFrag l <$> seq 0 bytes_per_addr.
Michael Sammler's avatar
Michael Sammler committed
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660

Lemma val_to_of_loc l :
  val_to_loc (val_of_loc l) = Some l.
Proof. simpl. by case_decide. Qed.

Lemma val_of_to_loc v l :
  val_to_loc v = Some l  v = val_of_loc l.
Proof.
  destruct v => //=; case_match => //; case_match => //.
  repeat (match goal with
  | |- context [ val_to_loc_go ?v _ _ ] => destruct v
          end => //=;
                  case_match => //; repeat (case_decide; subst => //=)).
  by case_match => // [[->]].
Qed.

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
661
(*+ [val_of_bool] and [i2v] *)
662
Definition i2v (n : Z) (it : int_type) : val := default [MPoison] (val_of_int n it).
Michael Sammler's avatar
Michael Sammler committed
663
664
665
666
667
668
669

Definition val_of_bool (b : bool) : val := i2v (Z_of_bool b) bool_it.

Lemma val_of_int_bool b it:
  val_of_int (Z_of_bool b) it = Some (i2v (Z_of_bool b) it).
Proof.
  have [|? Hv] := val_of_int_is_some it (Z_of_bool b); last by rewrite /i2v Hv.
670
671
  rewrite /elem_of /int_elem_of_it.
  have ? := min_int_le_0 it. have ? := max_int_ge_127 it.
Michael Sammler's avatar
Michael Sammler committed
672
673
674
  split; destruct b => /=; lia.
Qed.

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
675
676
677
678
Lemma val_to_int_bool b :
  val_to_int (val_of_bool b) bool_it = Some (Z_of_bool b).
Proof. by destruct b. Qed.

Michael Sammler's avatar
Michael Sammler committed
679
Lemma i2v_bool_length b it:
680
  length (i2v (Z_of_bool b) it) = bytes_per_int it.
Michael Sammler's avatar
Michael Sammler committed
681
682
683
684
685
Proof. by have /val_of_int_length -> := val_of_int_bool b it. Qed.
Lemma i2v_bool_Some b it:
  val_to_int (i2v (Z_of_bool b) it) it = Some (Z_of_bool b).
Proof. apply val_to_of_int. apply val_of_int_bool. Qed.

Michael Sammler's avatar
Michael Sammler committed
686
687
688
689
690
691
Arguments val_to_int : simpl never.
Arguments val_of_int : simpl never.
Arguments val_to_loc : simpl never.
Arguments val_of_loc : simpl never.
Typeclasses Opaque val_to_loc val_of_loc val_to_int val_of_int val_of_bool.

692
693
(*** Substitution *)
Fixpoint subst (x : var_name) (v : val) (e : expr)  : expr :=
Michael Sammler's avatar
Michael Sammler committed
694
  match e with
695
696
697
698
699
700
701
702
703
  | Var y => if bool_decide (x = y) then Val v else Var y
  | Val v => Val v
  | UnOp op ot e => UnOp op ot (subst x v e)
  | BinOp op ot1 ot2 e1 e2 => BinOp op ot1 ot2 (subst x v e1) (subst x v e2)
  | CopyAllocId e1 e2 => CopyAllocId (subst x v e1) (subst x v e2)
  | Deref o l e => Deref o l (subst x v e)
  | Call e es => Call (subst x v e) (subst x v <$> es)
  | CAS ly e1 e2 e3 => CAS ly (subst x v e1) (subst x v e2) (subst x v e3)
  | Concat el => Concat (subst x v <$> el)
Michael Sammler's avatar
Michael Sammler committed
704
  | IfE ot e1 e2 e3 => IfE ot (subst x v e1) (subst x v e2) (subst x v e3)
705
706
  | SkipE e => SkipE (subst x v e)
  | StuckE => StuckE
Michael Sammler's avatar
Michael Sammler committed
707
708
  end.

Michael Sammler's avatar
Michael Sammler committed
709
710
711
712
Fixpoint subst_l (xs : list (var_name * val)) (e : expr)  : expr :=
  match xs with
  | (x, v)::xs' => subst_l xs' (subst x v e)
  | _ => e
Michael Sammler's avatar
Michael Sammler committed
713
714
  end.

Michael Sammler's avatar
Michael Sammler committed
715
Fixpoint subst_stmt (xs : list (var_name * val)) (s : stmt) : stmt :=
716
717
  match s with
  | Goto b => Goto b
Michael Sammler's avatar
Michael Sammler committed
718
719
720
721
  | Return e => Return (subst_l xs e)
  | Switch it e m' bs def => Switch it (subst_l xs e) m' (subst_stmt xs <$> bs) (subst_stmt xs def)
  | Assign o ly e1 e2 s => Assign o ly (subst_l xs e1) (subst_l xs e2) (subst_stmt xs s)
  | SkipS s => SkipS (subst_stmt xs s)
722
  | StuckS => StuckS
Michael Sammler's avatar
Michael Sammler committed
723
  | ExprS e s => ExprS (subst_l xs e) (subst_stmt xs s)
724
725
  end.

Michael Sammler's avatar
Michael Sammler committed
726
727
Definition subst_function (xs : list (var_name * val)) (f : function) : function := {|
  f_code := (subst_stmt xs) <$> f.(f_code);
728
729
730
  f_args := f.(f_args); f_init := f.(f_init); f_local_vars := f.(f_local_vars);
|}.

Michael Sammler's avatar
Michael Sammler committed
731
732
733
(*** Evaluation of operations *)

(* evaluation can be non-deterministic for comparing pointers *)
734
735
Inductive eval_bin_op : bin_op  op_type  op_type  state  val  val  val  Prop :=
| PtrOffsetOpIP v1 v2 σ o l ly it:
Michael Sammler's avatar
Michael Sammler committed
736
737
738
739
    val_to_int v1 it = Some o 
    val_to_loc v2 = Some l 
    (* TODO: should we have an alignment check here? *)
    0  o 
740
    eval_bin_op (PtrOffsetOp ly) (IntOp it) PtrOp σ v1 v2 (val_of_loc (l offset{ly} o))
741
742
743
744
745
| PtrNegOffsetOpIP v1 v2 σ o l ly it:
    val_to_int v1 it = Some o 
    val_to_loc v2 = Some l 
    (* TODO: should we have an alignment check here? *)
    eval_bin_op (PtrNegOffsetOp ly) (IntOp it) PtrOp σ v1 v2 (val_of_loc (l offset{ly} -o))
746
| EqOpPNull v1 v2 σ l v:
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
747
    heap_state_loc_in_bounds l 0%nat σ.(st_heap) 
Michael Sammler's avatar
Michael Sammler committed
748
749
750
751
    val_to_loc v1 = Some l 
    val_to_int v2 size_t = Some 0 
    (* TODO ( see below ): Should we really hard code i32 here because of C? *)
    i2v (Z_of_bool false) i32 = v 
752
753
    eval_bin_op EqOp PtrOp PtrOp σ v1 v2 v
| NeOpPNull v1 v2 σ l v:
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
754
    heap_state_loc_in_bounds l 0%nat σ.(st_heap) 
Michael Sammler's avatar
Michael Sammler committed
755
756
757
    val_to_loc v1 = Some l 
    val_to_int v2 size_t = Some 0 
    i2v (Z_of_bool true) i32 = v 
758
759
    eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
| EqOpNullNull v1 v2 σ v:
Michael Sammler's avatar
Michael Sammler committed
760
761
762
    val_to_int v1 size_t = Some 0 
    val_to_int v2 size_t = Some 0 
    i2v (Z_of_bool true) i32 = v 
763
764
    eval_bin_op EqOp PtrOp PtrOp σ v1 v2 v
| NeOpNullNull v1 v2 σ v:
Michael Sammler's avatar
Michael Sammler committed
765
766
767
    val_to_int v1 size_t = Some 0 
    val_to_int v2 size_t = Some 0 
    i2v (Z_of_bool false) i32 = v 
768
    eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
769
| RelOpPP v1 v2 σ l1 l2 v b op:
Michael Sammler's avatar
Michael Sammler committed
770
771
    val_to_loc v1 = Some l1 
    val_to_loc v2 = Some l2 
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
772
    valid_ptr l1 σ.(st_heap)  valid_ptr l2 σ.(st_heap) 
773
774
775
776
777
778
779
780
781
    match op with
    | EqOp => Some (bool_decide (l1.2 = l2.2))
    | NeOp => Some (bool_decide (l1.2  l2.2))
    | LtOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 < l2.2)) else None
    | GtOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 > l2.2)) else None
    | LeOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 <= l2.2)) else None
    | GeOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 >= l2.2)) else None
    | _ => None
    end = Some b 
Michael Sammler's avatar
Michael Sammler committed
782
    i2v (Z_of_bool b) i32 = v 
783
    eval_bin_op op PtrOp PtrOp σ v1 v2 v
784
| RelOpII op v1 v2 σ n1 n2 it b:
Michael Sammler's avatar
Michael Sammler committed
785
786
787
788
789
790
791
792
793
794
795
796
797
    match op with
    | EqOp => Some (bool_decide (n1 = n2))
    | NeOp => Some (bool_decide (n1  n2))
    | LtOp => Some (bool_decide (n1 < n2))
    | GtOp => Some (bool_decide (n1 > n2))
    | LeOp => Some (bool_decide (n1 <= n2))
    | GeOp => Some (bool_decide (n1 >= n2))
    | _ => None
    end = Some b 
    val_to_int v1 it = Some n1 
    val_to_int v2 it = Some n2 
    (* TODO: What is the right int type of the result here? C seems to
    use i32 but maybe we don't want to hard code that. *)
798
799
    eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 (i2v (Z_of_bool b) i32)
| ArithOpII op v1 v2 σ n1 n2 it n v:
Michael Sammler's avatar
Michael Sammler committed
800
801
802
803
804
805
806
    match op with
    | AddOp => Some (n1 + n2)
    | SubOp => Some (n1 - n2)
    | MulOp => Some (n1 * n2)
    (* we need to take `quot` and `rem` here for the correct rounding
    behavior, i.e. rounding towards 0 (instead of `div` and `mod`,
    which round towards floor)*)
Fengmin Zhu's avatar
Ci/bits    
Fengmin Zhu committed
807
808
    | DivOp => if bool_decide (n2  0) then Some (n1 `quot` n2) else None
    | ModOp => if bool_decide (n2  0) then Some (n1 `rem` n2) else None
Michael Sammler's avatar
Michael Sammler committed
809
810
811
    | AndOp => Some (Z.land n1 n2)
    | OrOp => Some (Z.lor n1 n2)
    | XorOp => Some (Z.lxor n1 n2)
Fengmin Zhu's avatar
Ci/bits    
Fengmin Zhu committed
812
813
814
815
816
817
818
819
820
    (* For shift operators (`ShlOp` and `ShrOp`), behaviors are defined if:
       - lhs is nonnegative, and
       - rhs (also nonnegative) is less than the number of bits in lhs.
       See: https://en.cppreference.com/w/c/language/operator_arithmetic, "Shift operators". *)
    | ShlOp => if bool_decide (0  n1  0  n2 < bits_per_int it) then Some (n1  n2) else None
    (* NOTE: when lhs is negative, Coq's `≫` is not semantically equivalent to C's `>>`.
       Counterexample: Coq `-1000 ≫ 10 = 0`; C `-1000 >> 10 == -1`.
       This is because `≫` is implemented by `Z.div`. *)
    | ShrOp => if bool_decide (0  n1  0  n2 < bits_per_int it) then Some (n1  n2) else None
Michael Sammler's avatar
Michael Sammler committed
821
822
823
824
    | _ => None
    end = Some n 
    val_to_int v1 it = Some n1 
    val_to_int v2 it = Some n2 
825
    val_of_int (if it_signed it then n else n `mod` int_modulus it) it = Some v 
826
    eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 v
Michael Sammler's avatar
Michael Sammler committed
827
828
.

829
830
Inductive eval_un_op : un_op  op_type  state  val  val  Prop :=
| CastOpII itt its σ vs vt n:
Michael Sammler's avatar
Michael Sammler committed
831
832
    val_to_int vs its = Some n 
    val_of_int n itt = Some vt 
833
834
    eval_un_op (CastOp (IntOp itt)) (IntOp its) σ vs vt
| CastOpPP σ vs vt l:
Michael Sammler's avatar
Michael Sammler committed
835
836
    val_to_loc vs = Some l 
    val_of_loc l = vt 
837
    eval_un_op (CastOp PtrOp) PtrOp σ vs vt
838
839
840
841
842
843
844
845
| CastOpPI it σ vs vt l:
    val_to_loc vs = Some l 
    val_of_int l.2 it = Some vt 
    eval_un_op (CastOp (IntOp it)) PtrOp σ vs vt
| CastOpIP it σ vs vt n:
    val_to_int vs it = Some n 
    val_of_loc (None, n) = vt 
    eval_un_op (CastOp PtrOp) (IntOp it) σ vs vt
846
| NegOpI it σ vs vt n:
Michael Sammler's avatar
Michael Sammler committed
847
848
    val_to_int vs it = Some n 
    val_of_int (-n) it = Some vt 
849
    eval_un_op NegOp (IntOp it) σ vs vt
850
851
852
853
| NotIntOpI it σ vs vt n:
    val_to_int vs it = Some n 
    val_of_int (if it_signed it then Z.lnot n else Z_lunot (bits_per_int it) n) it = Some vt 
    eval_un_op NotIntOp (IntOp it) σ vs vt
Michael Sammler's avatar
Michael Sammler committed
854
855
856
857
.

(*** Evaluation of Expressions *)

858
Inductive expr_step : expr  state  list Empty_set  runtime_expr  state  list runtime_expr  Prop :=
Michael Sammler's avatar
Michael Sammler committed
859
860
861
| SkipES v σ:
    expr_step (SkipE (Val v)) σ [] (Val v) σ []
| UnOpS op v σ v' ot:
862
    eval_un_op op ot σ v v' 
Michael Sammler's avatar
Michael Sammler committed
863
864
    expr_step (UnOp op ot (Val v)) σ [] (Val v') σ []
| BinOpS op v1 v2 σ v' ot1 ot2:
865
    eval_bin_op op ot1 ot2 σ v1 v2 v' 
Michael Sammler's avatar
Michael Sammler committed
866
867
868
    expr_step (BinOp op ot1 ot2 (Val v1) (Val v2)) σ [] (Val v') σ []
| DerefS o v l ly v' σ:
    let start_st st :=  n, st = if o is Na2Ord then RSt (S n) else RSt n in
869
870
871
872
873
874
875
876
    let end_st st :=
      match o, st with
      | Na1Ord, Some (RSt n)     => RSt (S n)
      | Na2Ord, Some (RSt (S n)) => RSt n
      | ScOrd , Some st          => st
      |  _    , _                => WSt (* unreachable *)
      end
    in
Michael Sammler's avatar
Michael Sammler committed
877
878
    let end_expr := if o is Na1Ord then Deref Na2Ord ly (Val v) else Val v' in
    val_to_loc v = Some l 
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
879
    heap_at l ly v' start_st σ.(st_heap).(hs_heap) 
Michael Sammler's avatar
Michael Sammler committed
880
881
882
883
884
885
    expr_step (Deref o ly (Val v)) σ [] end_expr (heap_fmap (heap_upd l v' end_st) σ) []
(* TODO: look at CAS and see whether it makes sense. Also allow
comparing pointers? (see lambda rust) *)
(* corresponds to atomic_compare_exchange_strong, see https://en.cppreference.com/w/c/atomic/atomic_compare_exchange *)
| CasFailS l1 l2 vo ve σ z1 z2 v1 v2 v3 it:
    val_to_loc v1 = Some l1 
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
886
    heap_at l1 (it_layout it) vo (λ st,  n, st = RSt n) σ.(st_heap).(hs_heap) 
Michael Sammler's avatar
Michael Sammler committed
887
    val_to_loc v2 = Some l2 
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
888
    heap_at l2 (it_layout it) ve (λ st, st = RSt 0%nat) σ.(st_heap).(hs_heap) 
Michael Sammler's avatar
Michael Sammler committed
889
890
891
    val_to_int vo it = Some z1 
    val_to_int ve it = Some z2 
    v3 `has_layout_val` it_layout it 
892
    (bytes_per_int it  bytes_per_addr)%nat 
Michael Sammler's avatar
Michael Sammler committed
893
894
895
896
897
    z1  z2 
    expr_step (CAS (IntOp it) (Val v1) (Val v2) (Val v3)) σ []
              (Val (val_of_bool false)) (heap_fmap (heap_upd l2 vo (λ _, RSt 0%nat)) σ) []
| CasSucS l1 l2 it vo ve σ z1 z2 v1 v2 v3:
    val_to_loc v1 = Some l1 
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
898
    heap_at l1 (it_layout it) vo (λ st, st = RSt 0%nat) σ.(st_heap).(hs_heap) 
Michael Sammler's avatar
Michael Sammler committed
899
    val_to_loc v2 = Some l2 
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
900
    heap_at l2 (it_layout it) ve (λ st,  n, st = RSt n) σ.(st_heap).(hs_heap) 
Michael Sammler's avatar
Michael Sammler committed
901
902
903
    val_to_int vo it = Some z1 
    val_to_int ve it = Some z2 
    v3 `has_layout_val` it_layout it 
904
    (bytes_per_int it  bytes_per_addr)%nat 
Michael Sammler's avatar
Michael Sammler committed
905
906
907
    z1 = z2 
    expr_step (CAS (IntOp it) (Val v1) (Val v2) (Val v3)) σ []
              (Val (val_of_bool true)) (heap_fmap (heap_upd l1 v3 (λ _, RSt 0%nat)) σ) []
908
909
910
911
912
913
| CallS lsa lsv σ σ' σ'' vf vs f rf fn fn' :
    val_to_loc vf = Some f 
    σ.(st_fntbl) !! f = Some fn 
    length lsa = length fn.(f_args) 
    length lsv = length fn.(f_local_vars) 
    (* substitute the variables in fn with the corresponding locations *)
Michael Sammler's avatar
Michael Sammler committed
914
    fn' = subst_function (zip (fn.(f_args).*1 ++ fn.(f_local_vars).*1) (val_of_loc <$> (lsa ++ lsv))) fn 
915
916
917
918
919
920
    (* check the layout of the arguments *)
    Forall2 has_layout_val vs fn.(f_args).*2 
    (* ensure that locations are aligned *)
    Forall2 has_layout_loc lsa fn.(f_args).*2 
    Forall2 has_layout_loc lsv fn.(f_local_vars).*2 
    (* initialize the local vars to poison *)
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
921
922
    alloc_new_blocks σ.(st_heap) lsv ((λ p, replicate p.2.(ly_size) MPoison) <$> fn.(f_local_vars)) σ'.(st_heap) 
    σ.(st_fntbl) = σ'.(st_fntbl) 
923
    (* initialize the arguments with the supplied values *)
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
924
925
    alloc_new_blocks σ'.(st_heap) lsa vs σ''.(st_heap) 
    σ'.(st_fntbl) = σ''.(st_fntbl) 
926
927
928
929
930
931
932
933
    (* add used blocks allocations  *)
    rf = {| rf_fn := fn'; rf_locs := zip lsa fn.(f_args).*2 ++ zip lsv fn.(f_local_vars).*2; |} 
    expr_step (Call (Val vf) (Val <$> vs)) σ [] (to_rtstmt rf (Goto fn'.(f_init))) σ'' []
| CallFailS σ vf vs f fn:
    val_to_loc vf = Some f 
    σ.(st_fntbl) !! f = Some fn 
    Forall2 has_layout_val vs fn.(f_args).*2 
    expr_step (Call (Val vf) (Val <$> vs)) σ [] AllocFailed σ []
Michael Sammler's avatar
Michael Sammler committed
934
935
| ConcatS vs σ:
    expr_step (Concat (Val <$> vs)) σ [] (Val (mjoin vs)) σ []
936
937
938
939
| CopyAllocIdS l1 l2 v1 v2 σ:
    val_to_loc v1 = Some l1 
    val_to_loc v2 = Some l2 
    expr_step (CopyAllocId (Val v1) (Val v2)) σ [] (Val (val_of_loc (l2.1, l1.2))) σ []
Michael Sammler's avatar