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

Open Scope Z_scope.

9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
(** Representation of a standard (8-bit) byte. *)
Section Byte.
  Definition bits_per_byte : Z := 8.

  Definition byte_modulus : Z :=
    Eval cbv in 2 ^ bits_per_byte.

  Record byte :=
    Byte {
      byte_val : Z;
      byte_constr : -1 < byte_val < byte_modulus;
    }.

  Global Instance byte_eq_dec : EqDecision byte.
  Proof.
    move => [b1 H1] [b2 H2]. destruct (decide (b1 = b2)) as [->|].
    - left. assert (H1 = H2) as ->; [|done]. apply proof_irrel.
    - right. naive_solver.
  Qed.
Michael Sammler's avatar
Michael Sammler committed
28
29
30
31
32

  Program Definition byte0 : byte := {|
    byte_val := 0;
  |}.
  Next Obligation. done. Qed.
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
End Byte.

(** Representation of a type layout (byte size and alignment constraint). *)
Section Layout.
  Record layout :=
    Layout {
      ly_size : nat;
      ly_align_log : nat;
    }.

  Definition sizeof   (ly : layout) : nat := ly.(ly_size).
  Definition ly_align (ly : layout) : nat := 2 ^ ly.(ly_align_log).

  Global Instance layout_dec_eq : EqDecision layout.
  Proof. solve_decision. Defined.

  Global Instance layout_inhabited : Inhabited layout :=
    populate (Layout 0 0).

  Global Instance layout_countable : Countable layout.
  Proof.
    refine (inj_countable'
      (λ ly, (ly.(ly_size), ly.(ly_align_log)))
      (λ '(sz, a), Layout sz a) _); by intros [].
  Qed.

  Global Instance layout_le : SqSubsetEq layout := λ ly1 ly2,
    (ly1.(ly_size)  ly2.(ly_size))%nat 
    (ly1.(ly_align_log)  ly2.(ly_align_log))%nat.

  Global Instance layout_le_po : PreOrder layout_le.
  Proof.
    split => ?; rewrite /layout_le => *; repeat case_bool_decide => //; lia.
  Qed.

  Definition ly_offset (ly : layout) (n : nat) : layout := {|
    ly_size := ly.(ly_size) - n;
    (* Sadly we need to have the second argument to factor2 as we want
    that if l is aligned to x, then l + n * x is aligned to x for all n
    including 0. *)
    ly_align_log := ly.(ly_align_log) `min` factor2 n ly.(ly_align_log)
  |}.

  Definition ly_set_size (ly : layout) (n : nat) : layout := {|
    ly_size := n;
    ly_align_log := ly.(ly_align_log)
  |}.

  Definition ly_mult (ly : layout) (n : nat) : layout := {|
    ly_size := ly.(ly_size) * n;
    ly_align_log := ly.(ly_align_log)
  |}.

  Definition ly_with_align (sz : nat) (align : nat) : layout := {|
    ly_size := sz;
    ly_align_log := factor2 align 0
  |}.

  Definition layout_wf (ly : layout) : Prop := (ly_align ly | ly.(ly_size)).

  Lemma layout_wf_mod (ly : layout) :
    ly.(ly_size) `mod` ly_align ly = 0  layout_wf ly.
  Proof.
    move => ?. apply Z.mod_divide => //. have ->: 0 = O by [].
    move => /Nat2Z.inj/Nat.pow_nonzero. lia.
  Qed.

  Class LayoutWf (ly : layout) : Prop := layout_wf_wf : layout_wf ly.

  (* Class required because the combinators of layout are made typeclass opaque
     later, so TCEq does not work. *)
  Class LayoutEq (ly1 ly2 : layout) : Prop := layout_eq : ly1 = ly2.
End Layout.
Michael Sammler's avatar
Michael Sammler committed
106
107
108

Arguments ly_size : simpl never.
Arguments sizeof _ /.
109
(*Arguments ly_align_log : simpl never.*)
Michael Sammler's avatar
Michael Sammler committed
110
111
Arguments ly_align : simpl never.

112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
Typeclasses Opaque layout_le ly_offset ly_set_size ly_mult ly_with_align.

Hint Extern 0 (LayoutWf _) => refine (layout_wf_mod _ _); done : typeclass_instances.
Hint Extern 0 (LayoutWf _) => unfold LayoutWf; done : typeclass_instances.
Hint Extern 0 (LayoutEq _ _) => exact: eq_refl : typeclass_instances.

(** Representation of an integer type (size and signedness). *)
Section IntType.
  Definition signed := bool.

  Record int_type :=
    IntType {
      it_byte_size_log : nat;
      it_signed : signed;
    }.

  Definition bytes_per_int (it : int_type) : nat :=
    2 ^ it.(it_byte_size_log).

  Lemma bytes_per_int_gt_0 it : bytes_per_int it > 0.
  Proof.
    rewrite /bytes_per_int. move: it => [log ?] /=.
    rewrite Z2Nat_inj_pow. assert (0 < 2%nat ^ log); last lia.
    apply Z.pow_pos_nonneg; lia.
  Qed.

  Definition bits_per_int (it : int_type) : Z :=
    bytes_per_int it * bits_per_byte.

Fengmin Zhu's avatar
Ci/bits    
Fengmin Zhu committed
141
142
143
144
145
146
147
  Lemma bits_per_int_gt_0 it : bits_per_int it > 0.
  Proof.
    rewrite /bits_per_int /bits_per_byte.
    suff : (bytes_per_int it > 0) by lia.
    by apply: bytes_per_int_gt_0.
  Qed.

148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
  Definition int_modulus (it : int_type) : Z :=
    2 ^ bits_per_int it.

  Definition int_half_modulus (it : int_type) : Z :=
    2 ^ (bits_per_int it - 1).

  Lemma int_modulus_twice_half_modulus (it : int_type) :
    int_modulus it = 2 * int_half_modulus it.
  Proof.
    rewrite /int_modulus /int_half_modulus.
    rewrite -[X in X * _]Z.pow_1_r -Z.pow_add_r; try f_equal; try lia.
    rewrite /bits_per_int /bytes_per_int.
    apply Z.le_add_le_sub_l. rewrite Z.add_0_r.
    rewrite Z2Nat_inj_pow.
    assert (0 < 2%nat ^ it_byte_size_log it * bits_per_byte); last lia.
    apply Z.mul_pos_pos; last (rewrite /bits_per_byte; lia).
    apply Z.pow_pos_nonneg; lia.
  Qed.

  (* Minimal representable integer. *)
  Definition min_int (it : int_type) : Z :=
    if it.(it_signed) then - int_half_modulus it else 0.

  (* Maximal representable integer. *)
  Definition max_int (it : int_type) : Z :=
    (if it.(it_signed) then int_half_modulus it else int_modulus it) - 1.

  Lemma min_int_le_0 (it : int_type) : min_int it  0.
  Proof.
    have ? := bytes_per_int_gt_0 it. rewrite /min_int /int_half_modulus.
    destruct (it_signed it) => //. trans (- 2 ^ 7) => //.
    rewrite -Z.opp_le_mono. apply Z.pow_le_mono_r => //.
    rewrite /bits_per_int /bits_per_byte. lia.
  Qed.

  Lemma max_int_ge_127 (it : int_type) : 127  max_int it.
  Proof.
    have ? := bytes_per_int_gt_0 it.
    rewrite /max_int /int_modulus /int_half_modulus.
    rewrite /bits_per_int /bits_per_byte.
    have ->: (127 = 2 ^ 7 - 1) by []. apply Z.sub_le_mono => //.
    destruct (it_signed it); apply Z.pow_le_mono_r; lia.
  Qed.

  Global Instance int_elem_of_it : ElemOf Z int_type :=
    λ z it, min_int it  z  max_int it.

Michael Sammler's avatar
Michael Sammler committed
195
196
197
198
199
200
201
202
203
204
205
206
  Lemma int_modulus_mod_in_range n it:
    it_signed it = false 
    (n `mod` int_modulus it)  it.
  Proof.
    move => ?.
    have [|??]:= Z.mod_pos_bound n (int_modulus it). {
      apply: Z.pow_pos_nonneg => //. rewrite /bits_per_int/bits_per_byte/=. lia.
    }
    destruct it as [? []] => //.
    split; unfold min_int, max_int => /=; lia.
  Qed.

207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
  Definition it_layout (it : int_type) :=
    Layout (bytes_per_int it) it.(it_byte_size_log).

  Definition i8  := IntType 0 true.
  Definition u8  := IntType 0 false.
  Definition i16 := IntType 1 true.
  Definition u16 := IntType 1 false.
  Definition i32 := IntType 2 true.
  Definition u32 := IntType 2 false.
  Definition i64 := IntType 3 true.
  Definition u64 := IntType 3 false.

  (* hardcoding 64bit pointers for now *)
  Definition bytes_per_addr_log : nat := 3%nat.
  Definition bytes_per_addr : nat := (2 ^ bytes_per_addr_log)%nat.

223
224
  Definition intptr_t  := IntType bytes_per_addr_log true.
  Definition uintptr_t := IntType bytes_per_addr_log false.
225

226
227
  Definition size_t  := uintptr_t.
  Definition ssize_t := intptr_t.
228
229
230
  Definition bool_it := u8.
End IntType.

Michael Sammler's avatar
Michael Sammler committed
231
Declare Scope loc_scope.
Michael Sammler's avatar
Michael Sammler committed
232
233
Delimit Scope loc_scope with L.
Open Scope loc_scope.
234

235
Definition alloc_id := Z.
236
Definition addr := Z.
237

238
239
240
Definition dummy_alloc_id : alloc_id := 0.

Definition loc : Set := option alloc_id * addr.
241
242
243
244
245
246
247
248
249
250
251
252
Bind Scope loc_scope with loc.

Inductive mbyte : Set :=
| MByte (b : byte)
| MPtrFrag (l : loc) (n : nat)
| MPoison.

Definition val : Set := list mbyte.
Bind Scope val_scope with val.

Inductive lock_state := WSt | RSt (n : nat).

253
Definition heap := gmap addr (alloc_id * lock_state * mbyte).
254

255
256
257
258
259
260
Record allocation :=
  Allocation {
    alloc_start : Z; (* First valid address. *)
    alloc_end : Z;   (* One-past-the-end address. *)
  }.

261
Definition allocs := gmap alloc_id allocation.
262
263
264



Michael Sammler's avatar
Michael Sammler committed
265
266
267
268
269
270
271
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.
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.

Michael Sammler's avatar
Michael Sammler committed
272
273
Typeclasses Opaque shift_loc offset_loc.

Michael Sammler's avatar
Michael Sammler committed
274
275
276
277
278
279
280
281
282
283
284
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.
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.
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 aligned_to : simpl never.
(* Arguments aligned_to_log : simpl never. *)
Arguments has_layout_loc : simpl never.
Arguments has_layout_val : simpl never.
285
Typeclasses Opaque aligned_to has_layout_loc has_layout_val.
Michael Sammler's avatar
Michael Sammler committed
286

287
288
289
290
291

(*** Definitions of the language *)
Definition label := string. (* make TC opaque and implement countable and eqdicision *)
Definition var_name := string.

Michael Sammler's avatar
Michael Sammler committed
292
293
294
295
296
297
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
298
| ShrOp | EqOp | NeOp | LtOp | GtOp | LeOp | GeOp
Michael Sammler's avatar
Michael Sammler committed
299
(* Ptr is the second argument and pffset the first *)
300
| PtrOffsetOp (ly : layout) | PtrNegOffsetOp (ly : layout).
Michael Sammler's avatar
Michael Sammler committed
301
302
303
304
305
306

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

307
308
Section expr.
Local Unset Elimination Schemes.
Michael Sammler's avatar
Michael Sammler committed
309
310
311
312
313
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)
314
| CopyAllocId (e1 : expr) (e2 : expr)
Michael Sammler's avatar
Michael Sammler committed
315
316
| Deref (o : order) (ly : layout) (e : expr)
| CAS (ot : op_type) (e1 e2 e3 : expr)
317
| Call (f : expr) (args : list expr)
Michael Sammler's avatar
Michael Sammler committed
318
| Concat (es : list expr)
Michael Sammler's avatar
Michael Sammler committed
319
| IfE (ot : op_type) (e1 e2 e3 : expr)
Michael Sammler's avatar
Michael Sammler committed
320
321
322
| SkipE (e : expr)
| StuckE (* stuck expression *)
.
323
324
325
326
327
328
329
330
331
332
333
334
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
335
  ( (ot : op_type) (e1 e2 e3 : expr), P e1  P e2  P e3  P (IfE ot e1 e2 e3)) 
336
337
338
339
340
341
342
343
344
345
346
347
348
  ( (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
349
350
351
352
353

(** 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 :=
354
| Goto (b : label)
Michael Sammler's avatar
Michael Sammler committed
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
| 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; ?*)
370
371
  f_code : gmap label stmt;
  f_init : label;
Michael Sammler's avatar
Michael Sammler committed
372
373
374
375
376
}.

(* TODO: put both function and bytes in the same heap or make pointers disjoint (current version is wrong)*)
Record state := {
  st_heap: heap;
377
  st_allocs: allocs;
Michael Sammler's avatar
Michael Sammler committed
378
379
380
381
382
383
384
385
386
387
388
  st_fntbl: gmap loc function;
}.

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);
}.

389
390
391
392
393
394
395
396
397
398
399
400
401
402
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
403
| RTIfE (ot : op_type) (e1 e2 e3 : runtime_expr)
404
405
406
407
408
409
410
411
412
413
414
| 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)
.
415

416
417
418
419
420
421
422
423
424
425
426
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
427
  | IfE ot e1 e2 e3 => RTIfE ot (to_rtexpr e1) (to_rtexpr e2) (to_rtexpr e3)
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
  | 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.
444

445
446
447
448
449
450
451
452
453
454
455
456
457
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
458

459
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
460
461
462
463
464
465

(*** Relating val to logical values *)
(* we use little endian *)
Fixpoint val_to_int_go v : option Z :=
match v with
| [] => Some 0
466
| (MByte b)::v' => z  val_to_int_go v'; Some (byte_modulus * z + b.(byte_val))
Michael Sammler's avatar
Michael Sammler committed
467
468
469
| _ => None
end.
Definition val_to_int (v : val) (it : int_type) : option Z :=
470
471
  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
472
473
474
475
476
  else None.

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

Definition val_of_int (z : Z) (it : int_type) : option val :=
482
483
484
  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
485
486
487
488
489
490
491
492
  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 :
493
  0  z < 2 ^ (sz * bits_per_byte) 
Michael Sammler's avatar
Michael Sammler committed
494
495
  val_to_int_go (val_of_int_go z sz) = Some z.
Proof.
496
  rewrite /bits_per_byte.
Michael Sammler's avatar
Michael Sammler committed
497
  elim: sz z => /=. 1: rewrite /Z.of_nat; move => ??; f_equal; lia.
498
  move => sz IH z [? Hlt]. rewrite IH /byte_modulus /= -?Z_div_mod_eq //.
Michael Sammler's avatar
Michael Sammler committed
499
500
501
502
503
504
  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:
505
  val_of_int z it = Some v  length v = bytes_per_int it.
Michael Sammler's avatar
Michael Sammler committed
506
507
508
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:
509
  val_to_int v it = Some z  length v = bytes_per_int it.
Michael Sammler's avatar
Michael Sammler committed
510
511
512
Proof. rewrite /val_to_int. by case_decide. Qed.

Lemma val_of_int_is_some it z:
513
  z  it  is_Some (val_of_int z it).
Michael Sammler's avatar
Michael Sammler committed
514
515
516
Proof. rewrite /val_of_int. case_bool_decide; by eauto. Qed.

Lemma val_of_int_in_range it z v:
517
  val_of_int z it = Some v  z  it.
Michael Sammler's avatar
Michael Sammler committed
518
519
520
Proof. rewrite /val_of_int. case_bool_decide; by eauto. Qed.

Lemma val_to_of_int z it v:
521
  val_of_int z it = Some v  val_to_int v it = Some z.
Michael Sammler's avatar
Michael Sammler committed
522
523
Proof.
  rewrite /val_of_int /val_to_int => Ht.
524
525
526
527
  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
528
  rewrite val_of_int_go_length val_to_of_int_go /=.
529
530
531
532
533
534
535
536
537
538
539
540
  - 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.
541
      rewrite /bits_per_int /bytes_per_int /bits_per_byte /=.
542
543
      apply Z.pow_lt_mono_r; try lia.
    + rewrite /int_modulus /bits_per_int in HM. lia.
Michael Sammler's avatar
Michael Sammler committed
544
545
Qed.

546
547
548
549
550
551
552
553
554
Lemma it_in_range_mod n it:
  n  it  it_signed it = false 
  n `mod` int_modulus it = n.
Proof.
  move => [??] ?. rewrite Z.mod_small //.
  destruct it as [? []] => //. unfold min_int, max_int in *. simpl in *.
  lia.
Qed.

Michael Sammler's avatar
Michael Sammler committed
555
556
Fixpoint val_to_loc_go (v : val) (pos : nat) (l : loc) : option loc :=
  match v with
557
  | (MPtrFrag l' pos')::v' =>
Michael Sammler's avatar
Michael Sammler committed
558
    if bool_decide (pos = pos'  l = l') then
559
      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
560
561
562
563
564
    else None
  | _ => None
  end.
Definition val_to_loc (v : val) : option loc :=
  match v with
565
  | (MPtrFrag l 0)::v' => val_to_loc_go v' 1%nat l
Michael Sammler's avatar
Michael Sammler committed
566
567
  | _ => None
  end.
568
Definition val_of_loc (l : loc) : val := MPtrFrag l <$> seq 0 bytes_per_addr.
Michael Sammler's avatar
Michael Sammler committed
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584

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.

585
Definition i2v (n : Z) (it : int_type) : val := default [MPoison] (val_of_int n it).
Michael Sammler's avatar
Michael Sammler committed
586
587
588
589
590
591
592

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.
593
594
  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
595
596
597
  split; destruct b => /=; lia.
Qed.

Michael Sammler's avatar
Michael Sammler committed
598
Lemma i2v_bool_length b it:
599
  length (i2v (Z_of_bool b) it) = bytes_per_int it.
Michael Sammler's avatar
Michael Sammler committed
600
601
602
603
604
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
605
606
607
608
609
610
611
612
613
614
615
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.


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
616
617
618
619
620
Definition zero_val (n : nat) : val :=
  replicate n (MByte byte0).
Arguments zero_val : simpl never.
Typeclasses Opaque zero_val.

Michael Sammler's avatar
Michael Sammler committed
621
622
623
624
625
(*** Properties of layouts and alignment *)
Lemma ly_align_log_ly_align_eq_iff ly1 ly2:
  ly_align_log ly1 = ly_align_log ly2  ly_align ly1 = ly_align ly2.
Proof. rewrite /ly_align. split; first naive_solver. move => /Nat.pow_inj_r. lia. Qed.

626
627
628
629
Lemma ly_align_log_ly_align_le_iff ly1 ly2:
  (ly_align_log ly1  ly_align_log ly2  ly_align ly1  ly_align ly2)%nat.
Proof. rewrite /ly_align. apply: Nat.pow_le_mono_r_iff. lia. Qed.

630
631
632
633
Lemma ly_size_ly_with_align m n :
  ly_size (ly_with_align m n) = m.
Proof. done. Qed.

Michael Sammler's avatar
Michael Sammler committed
634
635
636
637
638
639
640
641
642
643
644
645
Lemma ly_align_ly_with_align m n :
  ly_align (ly_with_align m n) = keep_factor2 n 1.
Proof. rewrite /ly_with_align/keep_factor2/factor2. by destruct (factor2' n). Qed.

Lemma ly_align_ly_offset ly n :
  ly_align (ly_offset ly n) = (ly_align ly `min` keep_factor2 n (ly_align ly))%nat.
Proof.
  rewrite /ly_align/keep_factor2/=/factor2. destruct (factor2' n) as [n'|] => /=; last by rewrite !Nat.min_id.
  destruct (decide (ly_align_log ly  n'))%nat;[rewrite !min_l|rewrite !min_r]; try lia;
    apply Nat.pow_le_mono_r; lia.
Qed.

646
647
648
649
Lemma ly_size_ly_set_size ly n:
  ly_size (ly_set_size ly n) = n.
Proof. done. Qed.

Michael Sammler's avatar
Michael Sammler committed
650
651
652
653
654
655
656
657
658
659
660
661
662
663
Lemma ly_align_ly_set_size ly n:
  ly_align (ly_set_size ly n) = ly_align ly.
Proof. done. Qed.

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.

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.

664
665
666
667
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.

Michael Sammler's avatar
Michael Sammler committed
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
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.

Lemma has_layout_ly_offset l (n : nat) ly:
  l `has_layout_loc` ly 
  (l + n) `has_layout_loc` ly_offset ly n.
Proof.
  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.
Qed.

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.


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.

Lemma aligned_to_add l (n : nat) x:
  (l + x * n) `aligned_to` n  l `aligned_to` n.
Proof.
696
  unfold aligned_to. destruct l => /=. rewrite Z.add_comm.
Michael Sammler's avatar
Michael Sammler committed
697
698
699
700
701
702
703
704
  split.
  - apply: Z.divide_add_cancel_r. by apply Z.divide_mul_r.
  - apply Z.divide_add_r. by apply Z.divide_mul_r.
Qed.

Lemma aligned_to_mult_eq l n1 n2 off:
  l `aligned_to` n2  (l + off) `aligned_to` (n1 * n2)  (n2 | off).
Proof.
705
  unfold aligned_to. destruct l => /= ??. apply: Z.divide_add_cancel_r => //.
Michael Sammler's avatar
Michael Sammler committed
706
707
708
709
710
  apply: (Zdivide_mult_l _ n1). by rewrite Z.mul_comm -Nat2Z.inj_mul.
Qed.

(*** Helper functions for accessing the heap *)

711
712
713
714
(* 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_loc_in_bounds (l : loc) (n : nat) (st : state) : Prop :=
715
716
717
718
719
   alloc_id alloc,
    l.1 = Some alloc_id 
    st.(st_allocs) !! alloc_id = Some alloc 
    alloc.(alloc_start)  l.2 
    l.2 + n  alloc.(alloc_end).
720

Michael Sammler's avatar
Michael Sammler committed
721
722
723
Fixpoint heap_at_go l v flk h : Prop :=
  match v with
  | [] => True
724
  | b::v' => ( lk, h !! l.2 = Some (default dummy_alloc_id l.1, lk, b)  flk lk)  heap_at_go (l + 1) v' flk h
Michael Sammler's avatar
Michael Sammler committed
725
726
727
  end.

Definition heap_at l ly v flk h : Prop :=
728
729
  is_Some l.1  l `has_layout_loc` ly  v `has_layout_val` ly  heap_at_go l v flk h.

730
731
Definition heap_block_alive (h : heap) (aid : alloc_id) : Prop :=
   a lk b, h !! a = Some (aid, lk, b).
Michael Sammler's avatar
Michael Sammler committed
732

733
734
Definition heap_range_free (h : heap) (a : addr) (n : nat) : Prop :=
   a', a  a' < a + n  h !! a' = None.
Michael Sammler's avatar
Michael Sammler committed
735

736
Fixpoint heap_upd l v (flk : option lock_state  lock_state) (h : heap) : heap :=
Michael Sammler's avatar
Michael Sammler committed
737
  match v with
738
739
  | b::v' => partial_alter (λ m, Some (default dummy_alloc_id l.1,
                                       flk (snd <$> (fst <$> m)), b)) l.2 (heap_upd (l + 1) v' flk h)
Michael Sammler's avatar
Michael Sammler committed
740
741
742
743
744
745
746
747
748
749
750
751
  | [] => h
  end.

Fixpoint heap_upd_list ls vs flk h : heap :=
  match ls, vs with
  | l::ls', v::vs' => heap_upd l v flk (heap_upd_list ls' vs' flk h)
  | _, _ => h
  end.

Fixpoint heap_free l n h : heap :=
  match n with
  | O => h
752
  | S n' => delete l.2 (heap_free (l + 1) n' h)
Michael Sammler's avatar
Michael Sammler committed
753
754
755
756
757
758
759
760
761
762
763
  end.

Fixpoint heap_free_list ls h : heap :=
  match ls with
  | (l, ly)::ls' => heap_free l ly.(ly_size) (heap_free_list ls' h)
  | _ => h
  end.

Definition heap_fmap f σ := {|
  st_heap := f σ.(st_heap);
  st_fntbl := σ.(st_fntbl);
764
  st_allocs := σ.(st_allocs);
Michael Sammler's avatar
Michael Sammler committed
765
766
|}.

767
768
769
770
771
772
773
774
775
776
(*** Allocation semantics *)
(* We reserve 0 for NULL. *)
Definition min_alloc_start : Z := 1.

(* 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.

Definition to_allocation (off : Z) (len : nat) : allocation :=
  Allocation off (off + len).

777
Definition allocation_in_range (a : allocation) : Prop :=
778
779
780
781
782
783
  min_alloc_start  a.(alloc_start)  a.(alloc_end)  max_alloc_end.

Inductive alloc_new_block : state  loc  val  state  Prop :=
| AllocNewBlock σ l aid v:
    l.1 = Some aid 
    σ.(st_allocs) !! aid = None 
784
785
786
787
    (* TODO: is the precondition really useful? It should follow from
    the previous. *)
    ¬ heap_block_alive σ.(st_heap) aid 
    allocation_in_range (to_allocation l.2 (length v)) 
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
    heap_range_free σ.(st_heap) l.2 (length v) 
    alloc_new_block σ l v {|
      st_heap   := heap_upd l v (λ _, RSt 0%nat) σ.(st_heap);
      st_allocs := <[aid := to_allocation l.2 (length v)]> σ.(st_allocs);
      st_fntbl  := σ.(st_fntbl);
    |}.

Inductive alloc_new_blocks : state  list loc  list val  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) σ''.

(*** Substitution *)
Fixpoint subst (x : var_name) (v : val) (e : expr)  : expr :=
Michael Sammler's avatar
Michael Sammler committed
805
  match e with
806
807
808
809
810
811
812
813
814
  | 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
815
  | IfE ot e1 e2 e3 => IfE ot (subst x v e1) (subst x v e2) (subst x v e3)
816
817
  | SkipE e => SkipE (subst x v e)
  | StuckE => StuckE
Michael Sammler's avatar
Michael Sammler committed
818
819
  end.

Michael Sammler's avatar
Michael Sammler committed
820
821
822
823
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
824
825
  end.

Michael Sammler's avatar
Michael Sammler committed
826
Fixpoint subst_stmt (xs : list (var_name * val)) (s : stmt) : stmt :=
827
828
  match s with
  | Goto b => Goto b
Michael Sammler's avatar
Michael Sammler committed
829
830
831
832
  | 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)
833
  | StuckS => StuckS
Michael Sammler's avatar
Michael Sammler committed
834
  | ExprS e s => ExprS (subst_l xs e) (subst_stmt xs s)
835
836
  end.

Michael Sammler's avatar
Michael Sammler committed
837
838
Definition subst_function (xs : list (var_name * val)) (f : function) : function := {|
  f_code := (subst_stmt xs) <$> f.(f_code);
839
840
841
  f_args := f.(f_args); f_init := f.(f_init); f_local_vars := f.(f_local_vars);
|}.

Michael Sammler's avatar
Michael Sammler committed
842
(*** Evaluation of operations *)
843
844
845
846
(** 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 : state) : Prop :=
   aid, l.1 = Some aid  heap_block_alive st.(st_heap) aid  heap_loc_in_bounds l 0 st.
Michael Sammler's avatar
Michael Sammler committed
847
848

(* evaluation can be non-deterministic for comparing pointers *)
849
850
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
851
852
853
854
    val_to_int v1 it = Some o 
    val_to_loc v2 = Some l 
    (* TODO: should we have an alignment check here? *)
    0  o 
855
    eval_bin_op (PtrOffsetOp ly) (IntOp it) PtrOp σ v1 v2 (val_of_loc (l offset{ly} o))
856
857
858
859
860
| 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))
861
862
| EqOpPNull v1 v2 σ l v:
    heap_loc_in_bounds l 0%nat σ 
Michael Sammler's avatar
Michael Sammler committed
863
864
865
866
    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 
867
868
869
    eval_bin_op EqOp PtrOp PtrOp σ v1 v2 v
| NeOpPNull v1 v2 σ l v:
    heap_loc_in_bounds l 0%nat σ 
Michael Sammler's avatar
Michael Sammler committed
870
871
872
    val_to_loc v1 = Some l 
    val_to_int v2 size_t = Some 0 
    i2v (Z_of_bool true) i32 = v 
873
874
    eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
| EqOpNullNull v1 v2 σ v:
Michael Sammler's avatar
Michael Sammler committed
875
876
877
    val_to_int v1 size_t = Some 0 
    val_to_int v2 size_t = Some 0 
    i2v (Z_of_bool true) i32 = v 
878
879
    eval_bin_op EqOp PtrOp PtrOp σ v1 v2 v
| NeOpNullNull v1 v2 σ v:
Michael Sammler's avatar
Michael Sammler committed
880
881
882
    val_to_int v1 size_t = Some 0 
    val_to_int v2 size_t = Some 0 
    i2v (Z_of_bool false) i32 = v 
883
    eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
884
| RelOpPP v1 v2 σ l1 l2 v b op:
Michael Sammler's avatar
Michael Sammler committed
885
886
    val_to_loc v1 = Some l1 
    val_to_loc v2 = Some l2 
887
888
889
890
891
892
893
894
895
896
    valid_ptr l1 σ  valid_ptr l2 σ 
    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
897
    i2v (Z_of_bool b) i32 = v 
898
    eval_bin_op op PtrOp PtrOp σ v1 v2 v
899
| RelOpII op v1 v2 σ n1 n2 it b:
Michael Sammler's avatar
Michael Sammler committed
900
901
902
903
904
905
906
907
908
909
910
911
912
    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. *)
913
914
    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
915
916
917
918
919
920
921
    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
922
923
    | 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
924
925
926
    | 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
927
928
929
930
931
932
933
934
935
    (* 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
936
937
938
939
    | _ => None
    end = Some n 
    val_to_int v1 it = Some n1 
    val_to_int v2 it = Some n2 
940
    val_of_int (if it_signed it then n else n `mod` int_modulus it) it = Some v 
941
    eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 v
Michael Sammler's avatar
Michael Sammler committed
942
943
.

944
945
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
946
947
    val_to_int vs its = Some n 
    val_of_int n itt = Some vt 
948
949
    eval_un_op (CastOp (IntOp itt)) (IntOp its) σ vs vt
| CastOpPP σ vs vt l:
Michael Sammler's avatar
Michael Sammler committed
950
951
    val_to_loc vs = Some l 
    val_of_loc l = vt 
952
    eval_un_op (CastOp PtrOp) PtrOp σ vs vt
953
954
955
956
957
958
959
960
| 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
961
| NegOpI it σ vs vt n:
Michael Sammler's avatar
Michael Sammler committed
962
963
    val_to_int vs it = Some n 
    val_of_int (-n) it = Some vt 
964
    eval_un_op NegOp (IntOp it) σ vs vt
Michael Sammler's avatar
Michael Sammler committed
965
966
967
968
.

(*** Evaluation of Expressions *)

969
Inductive expr_step : expr  state  list Empty_set  runtime_expr  state  list runtime_expr  Prop :=
Michael Sammler's avatar
Michael Sammler committed
970
971
972
| SkipES v σ:
    expr_step (SkipE (Val v)) σ [] (Val v) σ []
| UnOpS op v σ v' ot:
973
    eval_un_op op ot σ v v' 
Michael Sammler's avatar
Michael Sammler committed
974
975
    expr_step (UnOp op ot (Val v)) σ [] (Val v') σ []
| BinOpS op v1 v2 σ v' ot1 ot2:
976
    eval_bin_op op ot1 ot2 σ v1 v2 v' 
Michael Sammler's avatar
Michael Sammler committed
977
978
979
    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
980
981
982
983
984
985
986
987
    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
988
989
990
991
992
993
994
995
996
997
998
999
1000
    let end_expr := if o is Na1Ord then Deref Na2Ord ly (Val v) else Val v' in
    val_to_loc v = Some l 
    heap_at l ly v' start_st σ.(st_heap) 
    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 
    heap_at l1 (it_layout it) vo (λ st,  n, st = RSt n) σ.(st_heap) 
    val_to_loc v2 = Some l2 
    heap_at l2 (it_layout it) ve (λ st, st = RSt 0%nat) σ.(st_heap) 
    val_to_int vo it = Some z1